1.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Fri Nov 18 13:50:01 2011 +0100
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Fri Nov 18 14:47:08 2011 +0100
     1.3 @@ -279,9 +279,13 @@
     1.4  
     1.5  val metis_lam_transs = [hide_lamsN, lam_liftingN, combinatorsN]
     1.6  
     1.7 +fun set_opt _ x NONE = SOME x
     1.8 +  | set_opt get x (SOME x0) =
     1.9 +    error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x) ^
    1.10 +           ".")
    1.11  fun consider_opt s =
    1.12 -  if member (op =) metis_lam_transs s then apsnd (K (SOME s))
    1.13 -  else apfst (K (SOME [s]))
    1.14 +  if member (op =) metis_lam_transs s then apsnd (set_opt I s)
    1.15 +  else apfst (set_opt hd [s])
    1.16  
    1.17  val parse_metis_options =
    1.18    Scan.optional