--- a/src/HOL/Tools/Metis/metis_tactic.ML Fri Nov 18 13:50:01 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Fri Nov 18 14:47:08 2011 +0100
@@ -279,9 +279,13 @@
val metis_lam_transs = [hide_lamsN, lam_liftingN, combinatorsN]
+fun set_opt _ x NONE = SOME x
+ | set_opt get x (SOME x0) =
+ error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x) ^
+ ".")
fun consider_opt s =
- if member (op =) metis_lam_transs s then apsnd (K (SOME s))
- else apfst (K (SOME [s]))
+ if member (op =) metis_lam_transs s then apsnd (set_opt I s)
+ else apfst (set_opt hd [s])
val parse_metis_options =
Scan.optional