# HG changeset patch
# User wenzelm
# Date 1256502946 -3600
# Node ID b8ca12f6681a0b5713d30543a58feedbdabb9e70
# Parent  61ee96bc989550bdabbda0144b8b64c6e21b1cdf
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;

diff -r 61ee96bc9895 -r b8ca12f6681a src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -321,7 +321,7 @@
                 fns2 @ (flat (Library.drop (i + 1, case_dummy_fns))) )));
           val ([def_thm], thy') =
             thy
-            |> Sign.declare_const [] decl |> snd
+            |> Sign.declare_const decl |> snd
             |> (PureThy.add_defs false o map Thm.no_attributes) [def];
 
         in (defs @ [def_thm], thy')
diff -r 61ee96bc9895 -r b8ca12f6681a src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -85,7 +85,7 @@
             val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
                     (*Forms a lambda-abstraction over the formal parameters*)
             val (c, thy') =
-              Sign.declare_const [] ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
+              Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
             val cdef = cname ^ "_def"
             val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
             val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
diff -r 61ee96bc9895 -r b8ca12f6681a src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/Pure/Isar/class.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -237,7 +237,7 @@
         val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b;
       in
         thy
-        |> Sign.declare_const [] ((b, ty0), syn)
+        |> Sign.declare_const ((b, ty0), syn)
         |> snd
         |> pair ((Name.of_binding b, ty), (c, ty'))
       end;
diff -r 61ee96bc9895 -r b8ca12f6681a src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -21,10 +21,8 @@
 
   val begin: class list -> sort -> Proof.context -> Proof.context
   val init: class -> theory -> Proof.context
-  val declare: class -> Properties.T
-    -> (binding * mixfix) * term -> theory -> theory
-  val abbrev: class -> Syntax.mode -> Properties.T
-    -> (binding * mixfix) * term -> theory -> theory
+  val declare: class -> (binding * mixfix) * term -> theory -> theory
+  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
   val class_prefix: string -> string
   val refresh_syntax: class -> Proof.context -> Proof.context
   val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
@@ -325,7 +323,7 @@
 
 val class_prefix = Logic.const_of_class o Long_Name.base_name;
 
-fun declare class pos ((c, mx), dict) thy =
+fun declare class ((c, mx), dict) thy =
   let
     val morph = morphism thy class;
     val b = Morphism.binding morph c;
@@ -337,7 +335,7 @@
       |> map_types Type.strip_sorts;
   in
     thy
-    |> Sign.declare_const pos ((b, Type.strip_sorts ty'), mx)
+    |> Sign.declare_const ((b, Type.strip_sorts ty'), mx)
     |> snd
     |> Thm.add_def false false (b_def, def_eq)
     |>> Thm.varifyT
@@ -347,7 +345,7 @@
     |> Sign.add_const_constraint (c', SOME ty')
   end;
 
-fun abbrev class prmode pos ((c, mx), rhs) thy =
+fun abbrev class prmode ((c, mx), rhs) thy =
   let
     val morph = morphism thy class;
     val unchecks = these_unchecks thy [class];
@@ -358,7 +356,7 @@
     val rhs'' = map_types Logic.varifyT rhs';
   in
     thy
-    |> Sign.add_abbrev (#1 prmode) pos (b, rhs'')
+    |> Sign.add_abbrev (#1 prmode) (b, rhs'')
     |> snd
     |> Sign.add_const_constraint (c', SOME ty')
     |> Sign.notation true prmode [(Const (c', ty'), mx)]
diff -r 61ee96bc9895 -r b8ca12f6681a src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -639,7 +639,7 @@
     val ([pred_def], defs_thy) =
       thy
       |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
-      |> Sign.declare_const [] ((bname, predT), NoSyn) |> snd
+      |> Sign.declare_const ((bname, predT), NoSyn) |> snd
       |> PureThy.add_defs false
         [((Binding.map_name Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
     val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
diff -r 61ee96bc9895 -r b8ca12f6681a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -119,8 +119,7 @@
   val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
   val add_const_constraint: string * typ option -> Proof.context -> Proof.context
-  val add_abbrev: string -> Properties.T ->
-    binding * term -> Proof.context -> (term * term) * Proof.context
+  val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
   val revert_abbrev: string -> string -> Proof.context -> Proof.context
   val verbose: bool Unsynchronized.ref
   val setmp_verbose: ('a -> 'b) -> 'a -> 'b
@@ -133,9 +132,6 @@
   val prems_limit: int Unsynchronized.ref
   val pretty_ctxt: Proof.context -> Pretty.T list
   val pretty_context: Proof.context -> Pretty.T list
-  val query_type: Proof.context -> string -> Properties.T
-  val query_const: Proof.context -> string -> Properties.T
-  val query_class: Proof.context -> string -> Properties.T
 end;
 
 structure ProofContext: PROOF_CONTEXT =
@@ -1051,13 +1047,13 @@
       in cert_term ctxt (Const (c, T)); T end;
   in ctxt |> (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end;
 
-fun add_abbrev mode tags (b, raw_t) ctxt =
+fun add_abbrev mode (b, raw_t) ctxt =
   let
     val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
     val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
     val ((lhs, rhs), consts') = consts_of ctxt
-      |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (b, t);
+      |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode (b, t);
   in
     ctxt
     |> (map_consts o apfst) (K consts')
@@ -1383,14 +1379,4 @@
     verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts)))
   end;
 
-
-(* query meta data *)
-
-val query_type = Type.the_tags o tsig_of;
-
-fun query_const ctxt name =
-  Consts.the_tags (consts_of ctxt) name handle TYPE (msg, _, _) => error msg;
-
-fun query_class ctxt name = query_const ctxt (Logic.const_of_class name);
-
 end;
diff -r 61ee96bc9895 -r b8ca12f6681a src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -161,7 +161,7 @@
     val xs = map (fn ((b, T), _) => (Name.of_binding b, T)) vars;
 
     (*consts*)
-    val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
+    val (consts, consts_thy) = thy |> fold_map Theory.specify_const vars;
     val subst = Term.subst_atomic (map Free xs ~~ consts);
 
     (*axioms*)
diff -r 61ee96bc9895 -r b8ca12f6681a src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -187,8 +187,8 @@
   in
     not (is_class andalso (similar_body orelse class_global)) ?
       (Context.mapping_result
-        (Sign.add_abbrev PrintMode.internal [] arg)
-        (ProofContext.add_abbrev PrintMode.internal [] arg)
+        (Sign.add_abbrev PrintMode.internal arg)
+        (ProofContext.add_abbrev PrintMode.internal arg)
       #-> (fn (lhs' as Const (d, _), _) =>
           similar_body ?
             (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
@@ -214,13 +214,13 @@
                 if mx3 <> NoSyn then syntax_error c'
                 else LocalTheory.theory_result (Overloading.declare (c', U))
                   ##> Overloading.confirm b
-            | NONE => LocalTheory.theory_result (Sign.declare_const [] ((b, U), mx3))));
+            | NONE => LocalTheory.theory_result (Sign.declare_const ((b, U), mx3))));
     val (const, lthy') = lthy |> declare_const;
     val t = Term.list_comb (const, map Free xs);
   in
     lthy'
     |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default ((b, mx2), t))
-    |> is_class ? class_target ta (Class_Target.declare target [] ((b, mx1), t))
+    |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
     |> LocalDefs.add_def ((b, NoSyn), t)
   end;
 
@@ -241,17 +241,17 @@
   in
     lthy |>
      (if is_locale then
-        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal [] (b, global_rhs))
+        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs))
         #-> (fn (lhs, _) =>
           let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
             term_syntax ta (locale_const ta prmode ((b, mx2), lhs')) #>
-            is_class ? class_target ta (Class_Target.abbrev target prmode [] ((b, mx1), t'))
+            is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t'))
           end)
       else
         LocalTheory.theory
-          (Sign.add_abbrev (#1 prmode) [] (b, global_rhs) #-> (fn (lhs, _) =>
+          (Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) =>
            Sign.notation true prmode [(lhs, mx3)])))
-    |> ProofContext.add_abbrev PrintMode.internal [] (b, t) |> snd
+    |> ProofContext.add_abbrev PrintMode.internal (b, t) |> snd
     |> LocalDefs.fixed_abbrev ((b, NoSyn), t)
   end;
 
diff -r 61ee96bc9895 -r b8ca12f6681a src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/Pure/axclass.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -305,7 +305,7 @@
   in
     thy
     |> Sign.mandatory_path name_inst
-    |> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
+    |> Sign.declare_const ((Binding.name c', T'), NoSyn)
     |-> (fn const' as Const (c'', _) =>
       Thm.add_def false true
         (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
diff -r 61ee96bc9895 -r b8ca12f6681a src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/Pure/codegen.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -337,7 +337,7 @@
     val tc = Sign.intern_type thy s;
   in
     case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of
-      SOME (Type.LogicalType i, _) =>
+      SOME (Type.LogicalType i) =>
         if num_args_of (fst syn) > i then
           error ("More arguments than corresponding type constructor " ^ s)
         else
diff -r 61ee96bc9895 -r b8ca12f6681a src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/Pure/consts.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -16,7 +16,6 @@
   val the_type: T -> string -> typ                             (*exception TYPE*)
   val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
   val type_scheme: T -> string -> typ                          (*exception TYPE*)
-  val the_tags: T -> string -> Properties.T                    (*exception TYPE*)
   val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
   val the_constraint: T -> string -> typ                       (*exception TYPE*)
   val space_of: T -> Name_Space.T
@@ -30,9 +29,9 @@
   val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
-  val declare: bool -> Name_Space.naming -> Properties.T -> binding * typ -> T -> T
+  val declare: bool -> Name_Space.naming -> binding * typ -> T -> T
   val constrain: string * typ option -> T -> T
-  val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string -> Properties.T ->
+  val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string ->
     binding * term -> T -> (term * term) * T
   val revert_abbrev: string -> string -> T -> T
   val hide: bool -> string -> T -> T
@@ -47,7 +46,7 @@
 
 (* datatype T *)
 
-type decl = {T: typ, typargs: int list list, tags: Properties.T, authentic: bool};
+type decl = {T: typ, typargs: int list list, authentic: bool};
 type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
 
 datatype T = Consts of
@@ -71,7 +70,8 @@
 
 (* reverted abbrevs *)
 
-val empty_abbrevs = Item_Net.init (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u') #1;
+val empty_abbrevs =
+  Item_Net.init (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u') #1;
 
 fun insert_abbrevs mode abbrs =
   Symtab.map_default (mode, empty_abbrevs) (Item_Net.insert abbrs);
@@ -110,7 +110,6 @@
 val the_decl = #1 oo the_const;
 val type_scheme = #T oo the_decl;
 val type_arguments = #typargs oo the_decl;
-val the_tags = #tags oo the_decl;
 
 val is_monomorphic = null oo type_arguments;
 
@@ -232,10 +231,10 @@
 
 (* declarations *)
 
-fun declare authentic naming tags (b, declT) =
+fun declare authentic naming (b, declT) =
   map_consts (fn (decls, constraints, rev_abbrevs) =>
     let
-      val decl = {T = declT, typargs = typargs_of declT, tags = tags, authentic = authentic};
+      val decl = {T = declT, typargs = typargs_of declT, authentic = authentic};
       val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
     in (decls', constraints, rev_abbrevs) end);
 
@@ -267,7 +266,7 @@
 
 in
 
-fun abbreviate pp tsig naming mode tags (b, raw_rhs) consts =
+fun abbreviate pp tsig naming mode (b, raw_rhs) consts =
   let
     val cert_term = certify pp tsig false consts;
     val expand_term = certify pp tsig true consts;
@@ -286,7 +285,7 @@
   in
     consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
       let
-        val decl = {T = T, typargs = typargs_of T, tags = tags, authentic = true};
+        val decl = {T = T, typargs = typargs_of T, authentic = true};
         val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
         val (_, decls') = decls
           |> Name_Space.define true naming (b, (decl, SOME abbr));
diff -r 61ee96bc9895 -r b8ca12f6681a src/Pure/display.ML
--- a/src/Pure/display.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/Pure/display.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -146,14 +146,14 @@
       [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
 
     val tfrees = map (fn v => TFree (v, []));
-    fun pretty_type syn (t, (Type.LogicalType n, _)) =
+    fun pretty_type syn (t, (Type.LogicalType n)) =
           if syn then NONE
           else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
-      | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
+      | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'))) =
           if syn <> syn' then NONE
           else SOME (Pretty.block
             [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
-      | pretty_type syn (t, (Type.Nonterminal, _)) =
+      | pretty_type syn (t, Type.Nonterminal) =
           if not syn then NONE
           else SOME (prt_typ (Type (t, [])));
 
diff -r 61ee96bc9895 -r b8ca12f6681a src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/Pure/sign.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -90,10 +90,10 @@
   val del_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
   val del_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
-  val declare_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
+  val declare_const: (binding * typ) * mixfix -> theory -> term * theory
   val add_consts: (binding * string * mixfix) list -> theory -> theory
   val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
-  val add_abbrev: string -> Properties.T -> binding * term -> theory -> (term * term) * theory
+  val add_abbrev: string -> binding * term -> theory -> (term * term) * theory
   val revert_abbrev: string -> string -> theory -> theory
   val add_const_constraint: string * typ option -> theory -> theory
   val primitive_class: binding * class list -> theory -> theory
@@ -434,7 +434,7 @@
   let
     val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Name.of_binding a, n, mx)) types) syn;
     val decls = map (fn (a, n, mx) => (Binding.map_name (Syntax.type_name mx) a, n)) types;
-    val tsig' = fold (Type.add_type naming []) decls tsig;
+    val tsig' = fold (Type.add_type naming) decls tsig;
   in (naming, syn', tsig', consts) end);
 
 
@@ -443,7 +443,7 @@
 fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   let
     val syn' = Syntax.update_consts (map Name.of_binding ns) syn;
-    val tsig' = fold (Type.add_nonterminal naming []) ns tsig;
+    val tsig' = fold (Type.add_nonterminal naming) ns tsig;
   in (naming, syn', tsig', consts) end);
 
 
@@ -457,7 +457,7 @@
       val b = Binding.map_name (Syntax.type_name mx) a;
       val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
         handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
-      val tsig' = Type.add_abbrev naming [] abbr tsig;
+      val tsig' = Type.add_abbrev naming abbr tsig;
     in (naming, syn', tsig', consts) end);
 
 val add_tyabbrs = fold (gen_add_tyabbr Syntax.parse_typ);
@@ -495,7 +495,7 @@
 
 local
 
-fun gen_add_consts parse_typ authentic tags raw_args thy =
+fun gen_add_consts parse_typ authentic raw_args thy =
   let
     val ctxt = ProofContext.init thy;
     val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
@@ -512,20 +512,20 @@
     val args = map prep raw_args;
   in
     thy
-    |> map_consts (fold (Consts.declare authentic (naming_of thy) tags o #1) args)
+    |> map_consts (fold (Consts.declare authentic (naming_of thy) o #1) args)
     |> add_syntax_i (map #2 args)
     |> pair (map #3 args)
   end;
 
 in
 
-fun add_consts args = snd o gen_add_consts Syntax.parse_typ false [] args;
-fun add_consts_i args = snd o gen_add_consts (K I) false [] args;
+fun add_consts args = snd o gen_add_consts Syntax.parse_typ false args;
+fun add_consts_i args = snd o gen_add_consts (K I) false args;
 
-fun declare_const tags ((b, T), mx) thy =
+fun declare_const ((b, T), mx) thy =
   let
     val pos = Binding.pos_of b;
-    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags [(b, T, mx)] thy;
+    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true [(b, T, mx)] thy;
     val _ = Position.report (Markup.const_decl c) pos;
   in (const, thy') end;
 
@@ -534,14 +534,14 @@
 
 (* abbreviations *)
 
-fun add_abbrev mode tags (b, raw_t) thy =
+fun add_abbrev mode (b, raw_t) thy =
   let
     val pp = Syntax.pp_global thy;
     val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
     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 (Binding.str_of b));
     val (res, consts') = consts_of thy
-      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (b, t);
+      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode (b, t);
   in (res, thy |> map_consts (K consts')) end;
 
 fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);
diff -r 61ee96bc9895 -r b8ca12f6681a src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/Pure/theory.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -35,7 +35,7 @@
   val add_defs: bool -> bool -> (binding * string) list -> theory -> theory
   val add_finals_i: bool -> term list -> theory -> theory
   val add_finals: bool -> string list -> theory -> theory
-  val specify_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
+  val specify_const: (binding * typ) * mixfix -> theory -> term * theory
 end
 
 structure Theory: THEORY =
@@ -219,8 +219,8 @@
     val name = if a = "" then (#1 lhs ^ " axiom") else a;
   in thy |> map_defs (dependencies thy false false name lhs rhs) end;
 
-fun specify_const tags decl thy =
-  let val (t as Const const, thy') = Sign.declare_const tags decl thy
+fun specify_const decl thy =
+  let val (t as Const const, thy') = Sign.declare_const decl thy
   in (t, add_deps "" const [] thy') end;
 
 
diff -r 61ee96bc9895 -r b8ca12f6681a src/Pure/type.ML
--- a/src/Pure/type.ML	Sun Oct 25 20:54:21 2009 +0100
+++ b/src/Pure/type.ML	Sun Oct 25 21:35:46 2009 +0100
@@ -16,7 +16,7 @@
   val rep_tsig: tsig ->
    {classes: Name_Space.T * Sorts.algebra,
     default: sort,
-    types: (decl * Properties.T) Name_Space.table,
+    types: decl Name_Space.table,
     log_types: string list}
   val empty_tsig: tsig
   val defaultS: tsig -> sort
@@ -39,7 +39,6 @@
   val cert_typ: tsig -> typ -> typ
   val arity_number: tsig -> string -> int
   val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
-  val the_tags: tsig -> string -> Properties.T
 
   (*special treatment of type vars*)
   val strip_sorts: typ -> typ
@@ -73,9 +72,9 @@
   val add_class: Pretty.pp -> Name_Space.naming -> binding * class list -> tsig -> tsig
   val hide_class: bool -> string -> tsig -> tsig
   val set_defsort: sort -> tsig -> tsig
-  val add_type: Name_Space.naming -> Properties.T -> binding * int -> tsig -> tsig
-  val add_abbrev: Name_Space.naming -> Properties.T -> binding * string list * typ -> tsig -> tsig
-  val add_nonterminal: Name_Space.naming -> Properties.T -> binding -> tsig -> tsig
+  val add_type: Name_Space.naming -> binding * int -> tsig -> tsig
+  val add_abbrev: Name_Space.naming -> binding * string list * typ -> tsig -> tsig
+  val add_nonterminal: Name_Space.naming -> binding -> tsig -> tsig
   val hide_type: bool -> string -> tsig -> tsig
   val add_arity: Pretty.pp -> arity -> tsig -> tsig
   val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
@@ -101,7 +100,7 @@
   TSig of {
     classes: Name_Space.T * Sorts.algebra,  (*order-sorted algebra of type classes*)
     default: sort,                          (*default sort on input*)
-    types: (decl * Properties.T) Name_Space.table,  (*declared types*)
+    types: decl Name_Space.table,           (*declared types*)
     log_types: string list};                (*logical types sorted by number of arguments*)
 
 fun rep_tsig (TSig comps) = comps;
@@ -112,7 +111,7 @@
 fun build_tsig (classes, default, types) =
   let
     val log_types =
-      Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (snd types) []
+      Symtab.fold (fn (c, LogicalType n) => cons (c, n) | _ => I) (snd types) []
       |> Library.sort (int_ord o pairself snd) |> map fst;
   in make_tsig (classes, default, types, log_types) end;
 
@@ -165,11 +164,6 @@
 
 fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
 
-fun the_tags tsig c =
-  (case lookup_type tsig c of
-    SOME (_, tags) => tags
-  | NONE => error (undecl_type c));
-
 
 (* certified types *)
 
@@ -197,13 +191,13 @@
             fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
           in
             (case lookup_type tsig c of
-              SOME (LogicalType n, _) => (nargs n; Type (c, Ts'))
-            | SOME (Abbreviation (vs, U, syn), _) =>
+              SOME (LogicalType n) => (nargs n; Type (c, Ts'))
+            | SOME (Abbreviation (vs, U, syn)) =>
                (nargs (length vs);
                 if syn then check_logical c else ();
                 if normalize then inst_typ (vs ~~ Ts') U
                 else Type (c, Ts'))
-            | SOME (Nonterminal, _) => (nargs 0; check_logical c; T)
+            | SOME Nonterminal => (nargs 0; check_logical c; T)
             | NONE => err (undecl_type c))
           end
       | cert (TFree (x, S)) = TFree (x, cert_sort tsig S)
@@ -224,7 +218,7 @@
 
 fun arity_number tsig a =
   (case lookup_type tsig a of
-    SOME (LogicalType n, _) => n
+    SOME (LogicalType n) => n
   | _ => error (undecl_type a));
 
 fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
@@ -525,7 +519,7 @@
   let
     val _ =
       (case lookup_type tsig t of
-        SOME (LogicalType n, _) => if length Ss <> n then error (bad_nargs t) else ()
+        SOME (LogicalType n) => if length Ss <> n then error (bad_nargs t) else ()
       | SOME _ => error ("Logical type constructor expected: " ^ quote t)
       | NONE => error (undecl_type t));
     val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
@@ -555,8 +549,8 @@
 
 local
 
-fun new_decl naming tags (c, decl) types =
-  #2 (Name_Space.define true naming (c, (decl, tags)) types);
+fun new_decl naming (c, decl) types =
+  #2 (Name_Space.define true naming (c, decl) types);
 
 fun map_types f = map_tsig (fn (classes, default, types) =>
   let
@@ -566,20 +560,21 @@
   in (classes, default, (space', tab')) end);
 
 fun syntactic types (Type (c, Ts)) =
-      (case Symtab.lookup types c of SOME (Nonterminal, _) => true | _ => false)
+      (case Symtab.lookup types c of SOME Nonterminal => true | _ => false)
         orelse exists (syntactic types) Ts
   | syntactic _ _ = false;
 
 in
 
-fun add_type naming tags (c, n) =
+fun add_type naming (c, n) =
   if n < 0 then error ("Bad type constructor declaration " ^ quote (Binding.str_of c))
-  else map_types (new_decl naming tags (c, LogicalType n));
+  else map_types (new_decl naming (c, LogicalType n));
 
-fun add_abbrev naming tags (a, vs, rhs) tsig = tsig |> map_types (fn types =>
+fun add_abbrev naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
   let
     fun err msg =
-      cat_error msg ("The error(s) above occurred in type abbreviation " ^ quote (Binding.str_of a));
+      cat_error msg ("The error(s) above occurred in type abbreviation " ^
+        quote (Binding.str_of a));
     val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs))
       handle TYPE (msg, _, _) => err msg;
     val _ =
@@ -590,9 +585,9 @@
       (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
         [] => []
       | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
-  in types |> new_decl naming tags (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
+  in types |> new_decl naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
 
-fun add_nonterminal naming tags = map_types o new_decl naming tags o rpair Nonterminal;
+fun add_nonterminal naming = map_types o new_decl naming o rpair Nonterminal;
 
 end;