src/HOL/Tools/transfer.ML

   in
     forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
   end
     handle TERM _ => thm
 
-fun abstract_equalities_transfer thm =
+fun abstract_equalities_transfer ctxt thm =
   let
     fun dest prop =
       let
         val prems = Logic.strip_imp_prems prop
         val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
         val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
       in
         (rel, fn rel' =>
           Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y)))
       end
-  in
-    gen_abstract_equalities dest thm
+    val contracted_eq_thm = 
+      Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
+      handle CTERM _ => thm
+  in
+    gen_abstract_equalities dest contracted_eq_thm
   end
 
 fun abstract_equalities_relator_eq rel_eq_thm =
   gen_abstract_equalities (fn x => (x, I))
     (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
 
-fun abstract_equalities_domain thm =
+fun abstract_equalities_domain ctxt thm =
   let
     fun dest prop =
       let
         val prems = Logic.strip_imp_prems prop
         val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
-        val ((dom, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
+        val ((eq, dom), y) = apfst Term.dest_comb (Term.dest_comb concl)
       in
-        (x, fn x' => Logic.list_implies (prems, HOLogic.mk_Trueprop (dom $ x' $ y)))
+        (dom, fn dom' => Logic.list_implies (prems, HOLogic.mk_Trueprop (eq $ dom' $ y)))
       end
-  in
-    gen_abstract_equalities dest thm
+    fun transfer_rel_conv conv = 
+      Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.arg1_conv (Conv.arg_conv conv)))
+    val contracted_eq_thm = 
+      Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
+  in
+    gen_abstract_equalities dest contracted_eq_thm
   end 
 
 
 (** Replacing explicit Domainp predicates with Domainp assumptions **)
 

     Conv.fconv_rule (Conv.prems_conv ~1 safe_transfer_rule_conv) thm
   end
 
 (** Adding transfer domain rules **)
 
-fun add_transfer_domain_thm thm = 
-  (add_transfer_thm o abstract_equalities_domain o detect_transfer_rules) thm
-
-fun del_transfer_domain_thm thm = 
-  (del_transfer_thm o abstract_equalities_domain o detect_transfer_rules) thm
+fun add_transfer_domain_thm thm ctxt = 
+  (add_transfer_thm o abstract_equalities_domain (Context.proof_of ctxt) o detect_transfer_rules) thm ctxt
+
+fun del_transfer_domain_thm thm ctxt = 
+  (del_transfer_thm o abstract_equalities_domain (Context.proof_of ctxt) o detect_transfer_rules) thm ctxt
 
 (** Transfer proof method **)
 
 val post_simps =
   @{thms transfer_forall_eq [symmetric]

 val transfer_prover_method : (Proof.context -> Method.method) context_parser =
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))
 
 (* Attribute for transfer rules *)
 
-val prep_rule = abstract_domains_transfer o abstract_equalities_transfer o Conv.fconv_rule prep_conv
+fun prep_rule ctxt thm = 
+  (abstract_domains_transfer o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv) thm
 
 val transfer_add =
-  Thm.declaration_attribute (add_transfer_thm o prep_rule)
+  Thm.declaration_attribute (fn thm => fn ctxt => 
+    (add_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)
 
 val transfer_del =
-  Thm.declaration_attribute (del_transfer_thm o prep_rule)
+  Thm.declaration_attribute (fn thm => fn ctxt => 
+    (del_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)
 
 val transfer_attribute =
   Attrib.add_del transfer_add transfer_del
 
 (* Attributes for transfer domain rules *)