# HG changeset patch
# User wenzelm
# Date 1191162033 -7200
# Node ID 6c7e94742afa5cd9da19ca08ee7402c5488133a0
# Parent  695a8e087b9f998c8e5a1682f3bff6224ec6ebd6
skofuns/absfuns: explicit markup as internal consts;

diff -r 695a8e087b9f -r 6c7e94742afa src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Sun Sep 30 16:20:31 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Sun Sep 30 16:20:33 2007 +0200
@@ -101,7 +101,8 @@
                 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
                         (*Forms a lambda-abstraction over the formal parameters*)
                 val _ = Output.debug (fn () => "declaring the constant " ^ cname)
-                val thy' = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy
+                val thy' =
+                  Sign.add_consts_authentic [Markup.property_internal] [(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'
@@ -273,7 +274,8 @@
                           val Ts = map type_of args
                           val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
                           val c = Const (Sign.full_name thy cname, cT)
-                          val thy = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy
+                          val thy =
+                            Sign.add_consts_authentic [Markup.property_internal] [(cname, cT, NoSyn)] thy
                                      (*Theory is augmented with the constant,
                                        then its definition*)
                           val cdef = cname ^ "_def"