src/HOL/Tools/Lifting/lifting_def.ML

             (binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm
           | _ => (relator_eq_onp_conv then_conv relator_eq_conv) ctm
       end
     
     val unfold_ret_val_invs = Conv.bottom_conv 
-      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args}))) lthy
+      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
     val cr_to_pcr_conv = Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)
     val unfold_inv_conv = 
       Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) lthy
     val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv 
       (cr_to_pcr_conv then_conv simp_arrows_conv))