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"