# HG changeset patch
# User wenzelm
# Date 1002202177 -7200
# Node ID b5b96188e94caa97eeeba3abbddcd2d2ccfbc82a
# Parent  afdbee613f582a16dea805beb964a5adaa5769a8
qualify MetaSimplifier;

diff -r afdbee613f58 -r b5b96188e94c src/ZF/Tools/inductive_package.ML
--- 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...";