# HG changeset patch
# User wenzelm
# Date 1423650377 -3600
# Node ID 7c433cca8fe0895eb2b4a80cc0026b8e406d57ee
# Parent  2a20354c08779ae7f87aa6cf60c3dac909cc8901
proper context;

diff -r 2a20354c0877 -r 7c433cca8fe0 src/HOL/Tools/Transfer/transfer.ML
--- 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