repaired inconsistency introduced in transiting to 'Local_Theory.define'

--- 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