diff -r 51ff2bc32774 -r fb9261990ffe src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Tue Aug 02 19:47:11 2005 +0200
+++ b/src/FOL/simpdata.ML	Tue Aug 02 19:47:12 2005 +0200
@@ -267,11 +267,11 @@
 end;
 
 val defEX_regroup =
-  Simplifier.simproc (Theory.sign_of (the_context ()))
+  Simplifier.simproc (the_context ())
     "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
 
 val defALL_regroup =
-  Simplifier.simproc (Theory.sign_of (the_context ()))
+  Simplifier.simproc (the_context ())
     "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
 
 
@@ -337,6 +337,10 @@
   setmksimps (mksimps mksimps_pairs)
   setmkcong mk_meta_cong;
 
+fun unfold_tac ss ths =
+  ALLGOALS (full_simp_tac
+    (Simplifier.inherit_bounds ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
+
 
 (*intuitionistic simprules only*)
 val IFOL_ss = FOL_basic_ss