# HG changeset patch
# User kuncar
# Date 1350425791 -7200
# Node ID b0d6d2e7a52269232331eb1dbccbedccdb5c2704
# Parent  9db36f881137b654282f6027d432bba591dec6ba
don't be so aggressive when expanding a transfer rule relation; rewrite only the relational part of the rule

diff -r 9db36f881137 -r b0d6d2e7a522 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue Oct 16 22:38:34 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Oct 17 00:16:31 2012 +0200
@@ -315,8 +315,10 @@
     val ((_, (_ , def_thm)), lthy') = 
       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})
-        |> Raw_Simplifier.rewrite_rule (Transfer.get_sym_relator_eq lthy')
+        |> 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)