--- a/src/ZF/UNITY/Constrains.ML Thu Jun 19 18:40:39 2003 +0200
+++ b/src/ZF/UNITY/Constrains.ML Fri Jun 20 12:10:45 2003 +0200
@@ -434,7 +434,7 @@
(*proves "co" properties when the program is specified*)
-fun constrains_tac i =
+fun gen_constrains_tac(cs,ss) i =
SELECT_GOAL
(EVERY [REPEAT (Always_Int_tac 1),
REPEAT (etac Always_ConstrainsI 1
@@ -445,14 +445,16 @@
(* Three subgoals *)
rewrite_goal_tac [st_set_def] 3,
REPEAT (Force_tac 2),
- full_simp_tac (simpset() addsimps !program_defs_ref) 1,
- ALLGOALS Clarify_tac,
+ full_simp_tac (ss addsimps !program_defs_ref) 1,
+ ALLGOALS (clarify_tac cs),
REPEAT (FIRSTGOAL (etac disjE)),
ALLGOALS Clarify_tac,
REPEAT (FIRSTGOAL (etac disjE)),
- ALLGOALS Clarify_tac,
- ALLGOALS Asm_full_simp_tac,
- ALLGOALS Clarify_tac]) i;
+ ALLGOALS (clarify_tac cs),
+ ALLGOALS (asm_full_simp_tac ss),
+ ALLGOALS (clarify_tac cs)]) i;
+
+fun constrains_tac st = gen_constrains_tac (claset(), simpset()) st;
(*For proving invariants*)
fun always_tac i =