# 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