Sign.add_consts_authentic: tags (Markup.property list);

--- a/src/HOL/Tools/datatype_abs_proofs.ML	Sun Sep 30 11:55:14 2007 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sun Sep 30 16:20:31 2007 +0200
@@ -320,7 +320,7 @@
                 fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
           val ([def_thm], thy') =
             thy
-            |> Sign.add_consts_authentic [decl]
+            |> Sign.add_consts_authentic [] [decl]
             |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
 
         in (defs @ [def_thm], thy')

--- a/src/HOL/Tools/datatype_package.ML	Sun Sep 30 11:55:14 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Sun Sep 30 16:20:31 2007 +0200
@@ -517,7 +517,7 @@
   end;
 
 val specify_consts = gen_specify_consts Sign.add_consts_i;
-val specify_consts_authentic = gen_specify_consts Sign.add_consts_authentic;
+val specify_consts_authentic = gen_specify_consts (Sign.add_consts_authentic []);
 
 structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
 val interpretation = DatatypeInterpretation.interpretation;

--- a/src/HOL/Tools/function_package/size.ML	Sun Sep 30 11:55:14 2007 +0200
+++ b/src/HOL/Tools/function_package/size.ML	Sun Sep 30 16:20:31 2007 +0200
@@ -31,7 +31,7 @@
       Const (Sign.full_name thy (Syntax.const_name c mx), T)) args;
   in
     thy
-    |> Sign.add_consts_authentic args
+    |> Sign.add_consts_authentic [] args
     |> Theory.add_finals_i false specs
   end;
 

--- a/src/Pure/Isar/class.ML	Sun Sep 30 11:55:14 2007 +0200
+++ b/src/Pure/Isar/class.ML	Sun Sep 30 16:20:31 2007 +0200
@@ -788,7 +788,7 @@
   in
     thy
     |> Sign.add_path prfx
-    |> Sign.add_consts_authentic [(c, ty', syn')]
+    |> Sign.add_consts_authentic [] [(c, ty', syn')]
     |> Sign.parent_path
     |> Sign.sticky_prefix prfx
     |> PureThy.add_defs_i false [(def, [])]

--- a/src/Pure/axclass.ML	Sun Sep 30 11:55:14 2007 +0200
+++ b/src/Pure/axclass.ML	Sun Sep 30 16:20:31 2007 +0200
@@ -371,7 +371,7 @@
     fun mk_const_name c = NameSpace.map_base (NameSpace.append prefix)
       (Sign.full_name thy c);
     fun add_const ((c, ty), syn) =
-      Sign.add_consts_authentic [(c, ty, syn)]
+      Sign.add_consts_authentic [] [(c, ty, syn)]
       #> pair (mk_const_name c, ty);
     fun mk_axioms cs thy =
       raw_dep_axioms thy cs

--- a/src/Pure/pure_thy.ML	Sun Sep 30 11:55:14 2007 +0200
+++ b/src/Pure/pure_thy.ML	Sun Sep 30 16:20:31 2007 +0200
@@ -499,7 +499,7 @@
     val def = Logic.mk_equals (list_comb (Const (c, ty), ts), t);
   in
     thy
-    |> Sign.add_consts_authentic [(raw_c, ty, syn)]
+    |> Sign.add_consts_authentic [] [(raw_c, ty, syn)]
     |> add_defs_i false [((name, def), atts)]
     |-> (fn [thm] => pair (c, thm))
   end;

--- a/src/Tools/code/code_package.ML	Sun Sep 30 11:55:14 2007 +0200
+++ b/src/Tools/code/code_package.ML	Sun Sep 30 16:20:31 2007 +0200
@@ -410,8 +410,7 @@
   let
     val naming = NameSpace.qualified_names NameSpace.default_naming;
     val consttab = Consts.empty
-      |> fold (fn c => Consts.declare naming
-           ((c, CodeFuncgr.typ funcgr c), true))
+      |> fold (fn c => Consts.declare true naming [] (c, CodeFuncgr.typ funcgr c))
            (CodeFuncgr.all funcgr);
     val algbr = (Code.operational_algebra thy, consttab);
   in