1.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Apr 10 17:48:17 2014 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Apr 10 17:48:18 2014 +0200
     1.3 @@ -121,7 +121,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 simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
    1.10      val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
    1.11      val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy