# HG changeset patch
# User wenzelm
# Date 1230892300 -3600
# Node ID 2c764235e041cb27d88f985de238bc81c7f228fd
# Parent  76af2a3c9d2803b418653e3dbb4ecf811181fd81
MetaSimplifier.SIMPLIFIER;

diff -r 76af2a3c9d28 -r 2c764235e041 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Fri Jan 02 11:31:07 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Fri Jan 02 11:31:40 2009 +0100
@@ -249,7 +249,7 @@
     |> ListPair.map (fn (t, tacs) =>
       Goal.prove_global thy1 [] [] t
         (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)))
-    handle Simplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg);
+    handle MetaSimplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg);
 
   (********)
   val dummy = writeln "  Proving the elimination rule...";