# HG changeset patch
# User wenzelm
# Date 1133470981 -3600
# Node ID d1c4b1112e33778383c096bcfabf57e10a59e9cf
# Parent  4365c8d84f69f633b70785fe0aa312cffa089ffb
unfold_tac: static evaluation of simpset;

diff -r 4365c8d84f69 -r d1c4b1112e33 src/FOL/simpdata.ML
--- 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*)
diff -r 4365c8d84f69 -r d1c4b1112e33 src/HOL/simpdata.ML
--- 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
diff -r 4365c8d84f69 -r d1c4b1112e33 src/ZF/OrdQuant.thy
--- 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
diff -r 4365c8d84f69 -r d1c4b1112e33 src/ZF/simpdata.ML
--- 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