# HG changeset patch
# User wenzelm
# Date 1159562819 -7200
# Node ID 17114542d2d4c7786ce0b7849a4c40d913b0206e
# Parent  18abee32d1b6f152adcc4bcc063e5633258bc58c
Sign.add_consts_authentic;

diff -r 18abee32d1b6 -r 17114542d2d4 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Fri Sep 29 22:46:57 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Fri Sep 29 22:46:59 2006 +0200
@@ -146,7 +146,7 @@
                 val c = Const (Sign.full_name thy cname, cT)
                 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
                         (*Forms a lambda-abstraction over the formal parameters*)
-                val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy
+                val thy' = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy
                            (*Theory is augmented with the constant, then its def*)
                 val cdef = cname ^ "_def"
                 val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy'
@@ -310,7 +310,7 @@
                           val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
                           val thy = theory_of_thm u'_th
                           val c = Const (Sign.full_name thy cname, cT)
-                          val thy = Theory.add_consts_i [(cname, cT, NoSyn)] thy
+                          val thy = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy
                                      (*Theory is augmented with the constant,
                                        then its definition*)
                           val cdef = cname ^ "_def"