Lists in strategies - without brackets?

[Tamarah Arons <tamarah@wisdom.weizmann.ac.il>]

Hello,

I am working with PVS 2.4

I have a strategy defined with the following parameters:

(defstep split-rho-all (&optional (values nil)(split-up 1)(inst-into -)
(force? f) (remove-impl? t)(no-sub? f)(split-all -)(hide? t))

The first parameter, values, is a list of values, e.g. 
("i!1" "j!1" "z") etc. The other parameters are seldom used.

However, users often omit the brackets over the values e.g.

 (split-rho-all "i!1" "j!1") instead of
 (split-rho-all ("i!1" "j!1")) 

which results in a segmentation fault:

Error: Received signal number 11 (Segmentation violation)
  [condition type: SYNCHRONOUS-OPERATING-SYSTEM-SIGNAL]

Is there any way to make PVS see that "j!1" is part of the values list?

The other parameters are always preceded by the formal name (i.e.
:split-up) when used, and I am willing that they always must be.
Even willing to exclude them from the strategy if necessary.

I.e. is there any way to allow (split-rho-all "i!1" "j!1")
to be interpreted with values as ("i!1" "j!1")?
Or, even better, to allow the user to type 
(split-rho-all "i!1" "j!1" :hide? f) and still bind values as ("i!1"
"j!1")?

Some inbuilt strategies allow lists to be given with or without brackets 
(e.g. hide). How can I do this?

Thanks,

Tamarah