1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Apr 10 17:48:17 2014 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Apr 10 17:48:18 2014 +0200
     1.3 @@ -534,7 +534,7 @@
     1.4        end
     1.5      
     1.6      val unfold_ret_val_invs = Conv.bottom_conv 
     1.7 -      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args}))) lthy
     1.8 +      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
     1.9      val cr_to_pcr_conv = Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)
    1.10      val unfold_inv_conv = 
    1.11        Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) lthy