1.1 --- a/src/HOL/Tools/res_axioms.ML	Sun Sep 30 16:20:31 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun Sep 30 16:20:33 2007 +0200
     1.3 @@ -101,7 +101,8 @@
     1.4                  val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
     1.5                          (*Forms a lambda-abstraction over the formal parameters*)
     1.6                  val _ = Output.debug (fn () => "declaring the constant " ^ cname)
     1.7 -                val thy' = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy
     1.8 +                val thy' =
     1.9 +                  Sign.add_consts_authentic [Markup.property_internal] [(cname, cT, NoSyn)] thy
    1.10                             (*Theory is augmented with the constant, then its def*)
    1.11                  val cdef = cname ^ "_def"
    1.12                  val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy'
    1.13 @@ -273,7 +274,8 @@
    1.14                            val Ts = map type_of args
    1.15                            val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
    1.16                            val c = Const (Sign.full_name thy cname, cT)
    1.17 -                          val thy = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy
    1.18 +                          val thy =
    1.19 +                            Sign.add_consts_authentic [Markup.property_internal] [(cname, cT, NoSyn)] thy
    1.20                                       (*Theory is augmented with the constant,
    1.21                                         then its definition*)
    1.22                            val cdef = cname ^ "_def"