--- a/src/HOL/Tools/ctr_sugar.ML Mon Dec 02 20:31:54 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar.ML Mon Dec 02 20:31:54 2013 +0100
@@ -503,7 +503,7 @@
if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
else pair (alternate_disc k, alternate_disc_no_def)
else if Binding.eq_name (b, equal_binding) then
- pair (rhs, refl)
+ pair (rhs, Thm.reflexive (certify lthy rhs))
else
Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs)) #>> apsnd snd
end) ks exist_xs_u_eq_ctrs disc_bindings