# HG changeset patch
# User wenzelm
# Date 1191162038 -7200
# Node ID 38afb780f6224f4c9ef19226031e3d957c457da0
# Parent  4f86d338411119e83f83a3b88fbaef233dcb19e2
add_consts_authentic/add_abbrev: tags (Markup.property list);
tuned signature;

diff -r 4f86d3384111 -r 38afb780f622 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Sep 30 16:20:37 2007 +0200
+++ b/src/Pure/sign.ML	Sun Sep 30 16:20:38 2007 +0200
@@ -161,9 +161,11 @@
   val simple_read_term: theory -> typ -> string -> term
   val read_term: theory -> string -> term
   val read_prop: theory -> string -> term
-  val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory
+  val add_consts_authentic: Markup.property list ->
+    (bstring * typ * mixfix) list -> theory -> theory
   val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
-  val add_abbrev: string -> bstring * term -> theory -> (term * term) * theory
+  val add_abbrev: string -> Markup.property list ->
+    bstring * term -> theory -> (term * term) * theory
   include SIGN_THEORY
   val add_const_constraint: string * typ option -> theory -> theory
   val primitive_class: string * class list -> theory -> theory
@@ -694,7 +696,7 @@
 
 local
 
-fun gen_add_consts prep_typ authentic raw_args thy =
+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;
     fun prep (raw_c, raw_T, raw_mx) =
@@ -703,18 +705,18 @@
         val c' = if authentic then Syntax.constN ^ full_name thy 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), authentic), (c', T, mx)) end;
+      in ((c, T), (c', T, mx)) end;
     val args = map prep raw_args;
   in
     thy
-    |> map_consts (fold (Consts.declare (naming_of thy) o #1) args)
+    |> map_consts (fold (Consts.declare authentic (naming_of thy) tags o #1) args)
     |> add_syntax_i (map #2 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 = 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;
 
 end;
@@ -722,7 +724,7 @@
 
 (* add abbreviations *)
 
-fun add_abbrev mode (c, raw_t) thy =
+fun add_abbrev mode tags (c, raw_t) thy =
   let
     val pp = pp thy;
     val prep_tm = Compress.term thy o no_frees pp o
@@ -731,7 +733,7 @@
     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
     val (res, consts') = consts_of thy
-      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode (c, t);
+      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (c, t);
   in (res, thy |> map_consts (K consts')) end;