# HG changeset patch
# User haftmann
# Date 1230906911 -3600
# Node ID 88d23c927e3791ea59239e2e377e350c750e9729
# Parent  2c764235e041cb27d88f985de238bc81c7f228fd# Parent  3eb95594ba89af72a92731c7214ef69d8b09c973
merged

diff -r 3eb95594ba89 -r 88d23c927e37 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Fri Jan 02 08:15:24 2009 +0100
+++ b/src/FOLP/IFOLP.thy	Fri Jan 02 15:35:11 2009 +0100
@@ -339,6 +339,7 @@
   shows "?a : R"
   apply (insert assms(1) [unfolded ex1_def])
   apply (erule exE conjE | assumption | rule assms(1))+
+  apply (erule assms(2), assumption)
   done
 
 
diff -r 3eb95594ba89 -r 88d23c927e37 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Fri Jan 02 08:15:24 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Fri Jan 02 15:35:11 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...";