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.
qualify MetaSimplifier;
authorwenzelm
Thu, 04 Oct 2001 15:29:37 +0200
changeset 11680 b5b96188e94c
parent 11679 afdbee613f58
child 11681 f5a7b4b203be
qualify MetaSimplifier;
src/ZF/Tools/inductive_package.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/Tools/inductive_package.ML	Thu Oct 04 15:29:22 2001 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Thu Oct 04 15:29:37 2001 +0200
@@ -262,7 +262,7 @@
   val intrs = ListPair.map prove_intr
 		(map (cterm_of sign1) intr_tms,
 		 map intro_tacsf (mk_disj_rls(length intr_tms)))
-	       handle SIMPLIFIER (msg,thm) => (print_thm thm; error msg);
+	       handle MetaSimplifier.SIMPLIFIER (msg,thm) => (print_thm thm; error msg);
 
   (********)
   val dummy = writeln "  Proving the elimination rule...";
isabelle