replaced Sign.add_consts_authentic by Sign.declare_const;

--- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 11 15:59:31 2007 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 11 16:05:23 2007 +0200
@@ -321,7 +321,7 @@
                 fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
           val ([def_thm], thy') =
             thy
-            |> Sign.add_consts_authentic [] [decl]
+            |> Sign.declare_const [] decl |> snd
             |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
 
         in (defs @ [def_thm], thy')

--- a/src/HOL/Tools/datatype_package.ML	Thu Oct 11 15:59:31 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Thu Oct 11 16:05:23 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 (fold (snd oo Sign.declare_const []));
 
 structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
 val interpretation = DatatypeInterpretation.interpretation;

--- a/src/HOL/Tools/res_axioms.ML	Thu Oct 11 15:59:31 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Thu Oct 11 16:05:23 2007 +0200
@@ -77,12 +77,11 @@
                 val argsx = map (fn T => Free(gensym"vsk", T)) extraTs
                 val args = argsx @ args0
                 val cT = extraTs ---> Ts ---> T
-                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 _ = Output.debug (fn () => "declaring the constant " ^ cname)
-                val thy' =
-                  Sign.add_consts_authentic [Markup.property_internal] [(cname, cT, NoSyn)] thy
+                val (c, thy') =
+                  Sign.declare_const [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 true false [(cdef, equals cT $ c $ rhs)] thy'

--- a/src/Pure/Isar/theory_target.ML	Thu Oct 11 15:59:31 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML	Thu Oct 11 16:05:23 2007 +0200
@@ -195,10 +195,10 @@
     fun const ((c, T), mx) thy =
       let
         val U = map #2 xs ---> T;
-        val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs);
         val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx;
         val mx3 = if is_loc then NoSyn else mx1;
-        val thy' = Sign.add_consts_authentic (ContextPosition.properties_of lthy) [(c, U, mx3)] thy;
+        val (const, thy') = Sign.declare_const (ContextPosition.properties_of lthy) (c, U, mx3) thy;
+        val t = Term.list_comb (const, map Free xs);
       in (((c, mx2), t), thy') end;
     fun const_class (SOME class) ((c, _), mx) (_, t) =
           LocalTheory.raw_theory_result (Class.add_const_in_class class ((c, t), mx))
@@ -227,7 +227,7 @@
   in
     lthy'
     |> fold2 (const_class some_class) decls abbrs
-    |> is_loc ? fold (internal_abbrev loc Syntax.default_mode) abbrs
+    |> is_loc ? fold (internal_abbrev loc Syntax.mode_default) abbrs
     |> LocalTheory.raw_theory (hide_abbrev some_class abbrs)
         (*FIXME abbreviations should never occur*)
     |> LocalDefs.add_defs defs

--- a/src/Pure/sign.ML	Thu Oct 11 15:59:31 2007 +0200
+++ b/src/Pure/sign.ML	Thu Oct 11 16:05:23 2007 +0200
@@ -156,8 +156,7 @@
   val simple_read_term: theory -> typ -> string -> term
   val read_term: theory -> string -> term
   val read_prop: theory -> string -> term
-  val add_consts_authentic: Markup.property list ->
-    (bstring * typ * mixfix) list -> theory -> theory
+  val declare_const: Markup.property list -> (bstring * typ * mixfix) -> theory -> term * theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
   val add_abbrev: string -> Markup.property list ->
     bstring * term -> theory -> (term * term) * theory
@@ -657,8 +656,8 @@
 
 val add_modesyntax = gen_add_syntax Syntax.parse_typ;
 val add_modesyntax_i = gen_add_syntax (K I);
-val add_syntax = add_modesyntax Syntax.default_mode;
-val add_syntax_i = add_modesyntax_i Syntax.default_mode;
+val add_syntax = add_modesyntax Syntax.mode_default;
+val add_syntax_i = add_modesyntax_i Syntax.mode_default;
 val del_modesyntax = gen_syntax Syntax.remove_const_gram Syntax.parse_typ;
 val del_modesyntax_i = gen_syntax Syntax.remove_const_gram (K I);
 
@@ -675,26 +674,30 @@
 
 fun gen_add_consts prep_typ authentic tags raw_args thy =
   let
-    val prepT = Compress.typ thy o Logic.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
+    val prepT = Type.no_tvars o Term.no_dummyT o prep_typ thy;
     fun prep (raw_c, raw_T, raw_mx) =
       let
         val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
-        val c' = if authentic then Syntax.constN ^ full_name thy c else c;
+        val full_c = full_name thy c;
+        val c' = if authentic then Syntax.constN ^ full_c else c;
         val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
           cat_error msg ("in declaration of constant " ^ quote c);
-      in ((c, T), (c', T, mx)) end;
+        val T' = Compress.typ thy (Logic.varifyT T);
+      in ((c, T'), (c', T', mx), Const (full_c, T)) end;
     val args = map prep raw_args;
   in
     thy
     |> map_consts (fold (Consts.declare authentic (naming_of thy) tags o #1) args)
     |> add_syntax_i (map #2 args)
+    |> pair (map #3 args)
   end;
 
 in
 
-val add_consts = gen_add_consts read_typ false [];
-val add_consts_i = gen_add_consts certify_typ false [];
-val add_consts_authentic = gen_add_consts certify_typ true;
+val add_consts = snd oo gen_add_consts read_typ false [];
+val add_consts_i = snd oo gen_add_consts certify_typ false [];
+
+fun declare_const tags arg = gen_add_consts certify_typ true tags [arg] #>> the_single;
 
 end;