# HG changeset patch
# User blanchet
# Date 1386012714 -3600
# Node ID 141cb34744dee35e0730ac0d226c0baa6b25e95e
# Parent  82a78bc9fa0d1d96bf3b351c2e056acacfff405d
repaired inconsistency introduced in transiting to 'Local_Theory.define'

diff -r 82a78bc9fa0d -r 141cb34744de src/HOL/Tools/ctr_sugar.ML
--- 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