src/HOL/Decision_Procs/MIR.thy
changeset 53168 d998de7f0efc
parent 51369 960b0ca9ae5d
child 54230 b1d955791529
--- a/src/HOL/Decision_Procs/MIR.thy	Fri Aug 23 15:36:54 2013 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Fri Aug 23 17:01:12 2013 +0200
@@ -5665,7 +5665,7 @@
 ML_file "mir_tac.ML"
 
 method_setup mir = {*
-  Args.mode "no_quantify" >>
+  Scan.lift (Args.mode "no_quantify") >>
     (fn q => fn ctxt => SIMPLE_METHOD' (Mir_Tac.mir_tac ctxt (not q)))
 *} "decision procedure for MIR arithmetic"