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