--- a/src/HOL/Tools/Transfer/transfer.ML Wed Feb 11 11:18:36 2015 +0100
+++ b/src/HOL/Tools/Transfer/transfer.ML Wed Feb 11 11:26:17 2015 +0100
@@ -611,13 +611,15 @@
|> Thm.instantiate (map tinst binsts, map inst binsts)
end
-fun eq_rules_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve0_tac eq_rules)
+fun eq_rules_tac ctxt eq_rules =
+ TRY o REPEAT_ALL_NEW (resolve_tac ctxt eq_rules)
THEN_ALL_NEW rtac @{thm is_equality_eq}
-fun eq_tac ctxt = eq_rules_tac (get_relator_eq_raw ctxt)
+fun eq_tac ctxt = eq_rules_tac ctxt (get_relator_eq_raw ctxt)
-fun transfer_step_tac ctxt = (REPEAT_ALL_NEW (resolve_tac ctxt (get_transfer_raw ctxt))
- THEN_ALL_NEW (DETERM o eq_rules_tac (get_relator_eq_raw ctxt)))
+fun transfer_step_tac ctxt =
+ REPEAT_ALL_NEW (resolve_tac ctxt (get_transfer_raw ctxt)
+ THEN_ALL_NEW (DETERM o eq_rules_tac ctxt (get_relator_eq_raw ctxt)))
fun transfer_tac equiv ctxt i =
let
@@ -635,7 +637,7 @@
THEN_ALL_NEW
(SOLVED'
(REPEAT_ALL_NEW (resolve_tac ctxt rules) THEN_ALL_NEW
- (DETERM o eq_rules_tac eq_rules))
+ (DETERM o eq_rules_tac ctxt eq_rules))
ORELSE' end_tac)) (i + 1)
handle TERM (_, ts) => raise TERM (err_msg, ts)
in
@@ -661,7 +663,7 @@
((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))
THEN_ALL_NEW
(REPEAT_ALL_NEW (resolve_tac ctxt rules) THEN_ALL_NEW
- (DETERM o eq_rules_tac eq_rules))) (i + 1),
+ (DETERM o eq_rules_tac ctxt eq_rules))) (i + 1),
rtac @{thm refl} i]
end)
@@ -689,7 +691,7 @@
(rtac rule
THEN_ALL_NEW
(SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
- THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
+ THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
handle TERM (_, ts) => raise TERM (err_msg, ts)
val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
val tnames = map (fst o dest_TFree o snd) instT
@@ -725,7 +727,7 @@
(rtac rule
THEN_ALL_NEW
(SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
- THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
+ THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
handle TERM (_, ts) => raise TERM (err_msg, ts)
val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
val tnames = map (fst o dest_TFree o snd) instT