--- a/src/HOL/Tools/Lifting/lifting_def.ML Wed Oct 24 17:40:56 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Wed Oct 24 18:43:25 2012 +0200
@@ -316,10 +316,8 @@
Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) lthy'
- val expand_rel_conv = Trueprop_conv (Conv.fun2_conv(top_rewr_conv (Transfer.get_sym_relator_eq lthy')))
val transfer_thm = ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
- |> Conv.fconv_rule expand_rel_conv
-
+
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)