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