Method.erule 0;
authorwenzelm
Wed Dec 27 18:27:19 2000 +0100 (2000-12-27 ago)
changeset 107438ea821d1e3a4
parent 10742 d27b0022b997
child 10744 5d142ca01b8e
Method.erule 0;
src/HOL/Tools/inductive_package.ML
     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