unfold_tac: static evaluation of simpset;

--- a/src/FOL/simpdata.ML	Thu Dec 01 18:45:24 2005 +0100
+++ b/src/FOL/simpdata.ML	Thu Dec 01 22:03:01 2005 +0100
@@ -338,9 +338,9 @@
   setmksimps (mksimps mksimps_pairs)
   setmkcong mk_meta_cong;
 
-fun unfold_tac ss ths =
-  ALLGOALS (full_simp_tac
-    (Simplifier.inherit_context ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
+fun unfold_tac ths =
+  let val ss0 = Simplifier.clear_ss FOL_basic_ss addsimps ths
+  in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
 
 
 (*intuitionistic simprules only*)

--- a/src/HOL/simpdata.ML	Thu Dec 01 18:45:24 2005 +0100
+++ b/src/HOL/simpdata.ML	Thu Dec 01 22:03:01 2005 +0100
@@ -350,9 +350,9 @@
     setmkeqTrue mk_eq_True
     setmkcong mk_meta_cong;
 
-fun unfold_tac ss ths =
-  ALLGOALS (full_simp_tac
-    (Simplifier.inherit_context ss (Simplifier.clear_ss HOL_basic_ss) addsimps ths));
+fun unfold_tac ths =
+  let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths
+  in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
 
 (*In general it seems wrong to add distributive laws by default: they
   might cause exponential blow-up.  But imp_disjL has been in for a while

--- a/src/ZF/OrdQuant.thy	Thu Dec 01 18:45:24 2005 +0100
+++ b/src/ZF/OrdQuant.thy	Thu Dec 01 22:03:01 2005 +0100
@@ -400,10 +400,12 @@
 ML_setup {*
 local
 
-fun prove_rex_tac ss = unfold_tac ss [rex_def] THEN Quantifier1.prove_one_point_ex_tac;
+val unfold_rex_tac = unfold_tac [rex_def];
+fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
 val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac;
 
-fun prove_rall_tac ss = unfold_tac ss [rall_def] THEN Quantifier1.prove_one_point_all_tac;
+val unfold_rall_tac = unfold_tac [rall_def];
+fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac;
 val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac;
 
 in

--- a/src/ZF/simpdata.ML	Thu Dec 01 18:45:24 2005 +0100
+++ b/src/ZF/simpdata.ML	Thu Dec 01 22:03:01 2005 +0100
@@ -55,10 +55,12 @@
 
 local
 
-fun prove_bex_tac ss = unfold_tac ss [Bex_def] THEN Quantifier1.prove_one_point_ex_tac;
+val unfold_bex_tac = unfold_tac [Bex_def];
+fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
 val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
 
-fun prove_ball_tac ss = unfold_tac ss [Ball_def] THEN Quantifier1.prove_one_point_all_tac;
+val unfold_ball_tac = unfold_tac [Ball_def];
+fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
 val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
 
 in