src/HOL/Tools/transfer.ML

 
 signature TRANSFER =
 sig
   val prep_conv: conv
   val get_relator_eq: Proof.context -> thm list
+  val get_sym_relator_eq: Proof.context -> thm list
   val transfer_add: attribute
   val transfer_del: attribute
   val transfer_rule_of_term: Proof.context -> term -> thm
   val transfer_tac: bool -> Proof.context -> int -> tactic
   val transfer_prover_tac: Proof.context -> int -> tactic

       relator_eq = Item_Net.merge (r1, r2) }
 )
 
 fun get_relator_eq ctxt = ctxt
   |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
-  |> map (Thm.symmetric o mk_meta_eq)
+  |> map safe_mk_meta_eq
+
+fun get_sym_relator_eq ctxt = ctxt
+  |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
+  |> map (Thm.symmetric o safe_mk_meta_eq)
 
 fun get_transfer_raw ctxt = ctxt
   |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
 
 fun get_known_frees ctxt = ctxt

 (* Tactic to correspond a value to itself *)
 fun eq_tac ctxt = SUBGOAL (fn (t, i) =>
   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_relator_eq ctxt
+    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
   in
     rtac thm2 i
   end handle Match => no_tac | TERM _ => no_tac)