diff -r 791157a4179a -r faf4afed009f src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Wed Oct 24 17:40:56 2012 +0200
+++ b/src/HOL/Tools/transfer.ML	Wed Oct 24 18:43:25 2012 +0200
@@ -85,20 +85,6 @@
 
 fun del_transfer_thm thm = Data.map (map_transfer_raw (Item_Net.remove thm))
 
-val relator_eq_setup =
-  let
-    val name = @{binding relator_eq}
-    fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm))
-    fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm))
-    val add = Thm.declaration_attribute add_thm
-    val del = Thm.declaration_attribute del_thm
-    val text = "declaration of relator equality rule (used by transfer method)"
-    val content = Item_Net.content o #relator_eq o Data.get
-  in
-    Attrib.setup name (Attrib.add_del add del) text
-    #> Global_Theory.add_thms_dynamic (name, content)
-  end
-
 (** Conversions **)
 
 val Rel_rule = Thm.symmetric @{thm Rel_def}
@@ -125,22 +111,60 @@
       else_conv
       Conv.all_conv) ct
 
-(** Transfer proof method **)
+(** Replacing explicit equalities with is_equality premises **)
+
+fun mk_is_equality t =
+  Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t
 
-fun RelT (Const (@{const_name Rel}, _) $ _ $ _ $ y) = fastype_of y
-  | RelT t = raise TERM ("RelT", [t])
+val is_equality_lemma =
+  @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (op =))"
+    by (unfold is_equality_def, rule, drule meta_spec,
+      erule meta_mp, rule refl, simp)}
 
-(* Tactic to correspond a value to itself *)
-fun eq_tac ctxt = SUBGOAL (fn (t, i) =>
+fun gen_abstract_equalities (dest : term -> term * (term -> term)) thm =
   let
-    val T = RelT (HOLogic.dest_Trueprop (Logic.strip_assums_concl t))
-    val cT = ctyp_of (Proof_Context.theory_of ctxt) T
-    val rews = get_sym_relator_eq ctxt
-    val thm1 = Drule.instantiate' [SOME cT] [] @{thm Rel_eq_refl}
-    val thm2 = Raw_Simplifier.rewrite_rule rews thm1
+    val thy = Thm.theory_of_thm thm
+    val prop = Thm.prop_of thm
+    val (t, mk_prop') = dest prop
+    val add_eqs = Term.fold_aterms
+      (fn t as Const (@{const_name HOL.eq}, _) => insert (op =) t | _ => I)
+    val eq_consts = rev (add_eqs t [])
+    val eqTs = map (snd o dest_Const) eq_consts
+    val used = Term.add_free_names prop []
+    val names = map (K "") eqTs |> Name.variant_list used
+    val frees = map Free (names ~~ eqTs)
+    val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
+    val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
+    val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
+    val cprop = Thm.cterm_of thy prop2
+    val equal_thm = Raw_Simplifier.rewrite false [is_equality_lemma] cprop
+    fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
   in
-    rtac thm2 i
-  end handle Match => no_tac | TERM _ => no_tac)
+    forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
+  end
+    handle TERM _ => thm
+
+fun abstract_equalities_transfer 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
+  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]})
+
+
+(** Transfer proof method **)
 
 val post_simps =
   @{thms transfer_forall_eq [symmetric]
@@ -273,7 +297,7 @@
          (rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t))
            THEN_ALL_NEW
              (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules))
-               ORELSE' eq_tac ctxt ORELSE' end_tac)) (i + 1)) i,
+               ORELSE' end_tac)) (i + 1)) i,
        (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
        rewrite_goal_tac post_simps i,
        rtac @{thm _} i]
@@ -289,8 +313,7 @@
       [CONVERSION prep_conv i,
        rtac @{thm transfer_prover_start} i,
        (rtac rule1 THEN_ALL_NEW
-         REPEAT_ALL_NEW
-           (resolve_tac rules ORELSE' eq_tac ctxt)) (i+1),
+         REPEAT_ALL_NEW (resolve_tac rules)) (i+1),
        rtac @{thm refl} i]
   end)
 
@@ -311,7 +334,7 @@
 
 (* Attribute for transfer rules *)
 
-val prep_rule = Conv.fconv_rule prep_conv
+val prep_rule = abstract_equalities_transfer o Conv.fconv_rule prep_conv
 
 val transfer_add =
   Thm.declaration_attribute (add_transfer_thm o prep_rule)
@@ -324,6 +347,22 @@
 
 (* Theory setup *)
 
+val relator_eq_setup =
+  let
+    val name = @{binding relator_eq}
+    fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm))
+      #> add_transfer_thm (abstract_equalities_relator_eq thm)
+    fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm))
+      #> del_transfer_thm (abstract_equalities_relator_eq thm)
+    val add = Thm.declaration_attribute add_thm
+    val del = Thm.declaration_attribute del_thm
+    val text = "declaration of relator equality rule (used by transfer method)"
+    val content = Item_Net.content o #relator_eq o Data.get
+  in
+    Attrib.setup name (Attrib.add_del add del) text
+    #> Global_Theory.add_thms_dynamic (name, content)
+  end
+
 val setup =
   relator_eq_setup
   #> Attrib.setup @{binding transfer_rule} transfer_attribute