# HG changeset patch
# User blanchet
# Date 1321624028 -3600
# Node ID 66f31d77b05f034c0a62d3782ed2f71f6651fe7f
# Parent  33b964e117bda276a24e7516641e9aa09ed85ed4
more robust options

diff -r 33b964e117bd -r 66f31d77b05f src/HOL/Tools/Metis/metis_tactic.ML
--- 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