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