# HG changeset patch
# User kuncar
# Date 1348770630 -7200
# Node ID 06cf80661e7a2e9ec3cf0c2408144e4d14eb40fa
# Parent  9d34cfe1dbdf793084bf7ec7ef29e238f1fa40e6
new get function for non-symmetric relator_eq & tuned

diff -r 9d34cfe1dbdf -r 06cf80661e7a src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Sep 27 19:35:29 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Sep 27 20:30:30 2012 +0200
@@ -316,7 +316,7 @@
       Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
 
     val transfer_thm = ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
-        |> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy')
+        |> Raw_Simplifier.rewrite_rule (Transfer.get_sym_relator_eq lthy')
      
     val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm
     val maybe_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty)
diff -r 9d34cfe1dbdf -r 06cf80661e7a src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Thu Sep 27 19:35:29 2012 +0200
+++ b/src/HOL/Tools/transfer.ML	Thu Sep 27 20:30:30 2012 +0200
@@ -8,6 +8,7 @@
 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
@@ -47,7 +48,11 @@
 
 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)
@@ -130,7 +135,7 @@
   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