Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Method.erule 0;
authorwenzelm
Wed, 27 Dec 2000 18:27:19 +0100
changeset 10743 8ea821d1e3a4
parent 10742 d27b0022b997
child 10744 5d142ca01b8e
Method.erule 0;
src/HOL/Tools/inductive_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/inductive_package.ML	Wed Dec 27 18:26:53 2000 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Wed Dec 27 18:27:19 2000 +0100
@@ -535,7 +535,7 @@
     val thy = ProofContext.theory_of ctxt;
     val ss = Simplifier.get_local_simpset ctxt;
     val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props;
-  in Method.erule (map (smart_mk_cases thy ss) cprops) end;
+  in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end;
 
 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
isabelle