--- 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)
--- 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