src/HOL/Tools/inductive.ML
changeset 46708 b138dee7bed3
parent 46219 426ed18eba43
child 46893 d5bb4c212df1
     1.1 --- a/src/HOL/Tools/inductive.ML	Mon Feb 27 15:42:07 2012 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Mon Feb 27 15:48:02 2012 +0100
     1.3 @@ -432,7 +432,7 @@
     1.4        in
     1.5          (Skip_Proof.prove ctxt'' [] prems P
     1.6            (fn {prems, ...} => EVERY
     1.7 -            [cut_facts_tac [hd prems] 1,
     1.8 +            [cut_tac (hd prems) 1,
     1.9               rewrite_goals_tac rec_preds_defs,
    1.10               dtac (unfold RS iffD1) 1,
    1.11               REPEAT (FIRSTGOAL (eresolve_tac rules1)),