src/HOL/Decision_Procs/mir_tac.ML
changeset 30509 e19d5b459a61
parent 30439 57c68b3af2ea
child 30939 207ec81543f6
     1.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Fri Mar 13 19:10:46 2009 +0100
     1.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri Mar 13 19:53:09 2009 +0100
     1.3 @@ -150,11 +150,10 @@
     1.4     Method.simple_args 
     1.5    (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
     1.6      curry (Library.foldl op |>) true)
     1.7 -    (fn q => fn ctxt => meth ctxt q 1)
     1.8 +    (fn q => fn ctxt => meth ctxt q)
     1.9    end;
    1.10  
    1.11 -fun mir_method ctxt q i = Method.METHOD (fn facts =>
    1.12 -  Method.insert_tac facts 1 THEN mir_tac ctxt q i);
    1.13 +fun mir_method ctxt q = SIMPLE_METHOD' (mir_tac ctxt q);
    1.14  
    1.15  val setup =
    1.16    Method.add_method ("mir",