src/HOL/Tools/inductive_package.ML
changeset 10743 8ea821d1e3a4
parent 10735 dfaf75f0076f
child 10804 306aee77eadd
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Dec 27 18:26:53 2000 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Dec 27 18:27:19 2000 +0100
     1.3 @@ -535,7 +535,7 @@
     1.4      val thy = ProofContext.theory_of ctxt;
     1.5      val ss = Simplifier.get_local_simpset ctxt;
     1.6      val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props;
     1.7 -  in Method.erule (map (smart_mk_cases thy ss) cprops) end;
     1.8 +  in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end;
     1.9  
    1.10  val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
    1.11