--- a/src/HOL/UNITY/UNITY_tactics.ML Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML Mon Nov 10 21:49:48 2014 +0100
@@ -6,7 +6,8 @@
*)
(*Combines two invariance ASSUMPTIONS into one. USEFUL??*)
-val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin}
+fun Always_Int_tac ctxt =
+ dtac @{thm Always_Int_I} THEN' assume_tac ctxt THEN' etac @{thm Always_thin}
(*Combines a list of invariance THEOREMS into one.*)
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})
@@ -16,7 +17,7 @@
fun constrains_tac ctxt i =
SELECT_GOAL
(EVERY
- [REPEAT (Always_Int_tac 1),
+ [REPEAT (Always_Int_tac ctxt 1),
(*reduce the fancy safety properties to "constrains"*)
REPEAT (etac @{thm Always_ConstrainsI} 1
ORELSE
@@ -35,7 +36,7 @@
fun ensures_tac ctxt sact =
SELECT_GOAL
(EVERY
- [REPEAT (Always_Int_tac 1),
+ [REPEAT (Always_Int_tac ctxt 1),
etac @{thm Always_LeadsTo_Basis} 1
ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},