--- 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