src/ZF/simpdata.ML
changeset 18324 d1c4b1112e33
parent 17876 b9c92f384109
child 18735 f5fd06394f17
--- 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