eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
authorwenzelm
Sun Oct 25 21:35:46 2009 +0100 (2009-10-25 ago)
changeset 33173b8ca12f6681a
parent 33172 61ee96bc9895
child 33174 1f2051f41335
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/res_axioms.ML
src/Pure/Isar/class.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/consts.ML
src/Pure/display.ML
src/Pure/sign.ML
src/Pure/theory.ML
src/Pure/type.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Oct 25 20:54:21 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Oct 25 21:35:46 2009 +0100
     1.3 @@ -321,7 +321,7 @@
     1.4                  fns2 @ (flat (Library.drop (i + 1, case_dummy_fns))) )));
     1.5            val ([def_thm], thy') =
     1.6              thy
     1.7 -            |> Sign.declare_const [] decl |> snd
     1.8 +            |> Sign.declare_const decl |> snd
     1.9              |> (PureThy.add_defs false o map Thm.no_attributes) [def];
    1.10  
    1.11          in (defs @ [def_thm], thy')
     2.1 --- a/src/HOL/Tools/res_axioms.ML	Sun Oct 25 20:54:21 2009 +0100
     2.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun Oct 25 21:35:46 2009 +0100
     2.3 @@ -85,7 +85,7 @@
     2.4              val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
     2.5                      (*Forms a lambda-abstraction over the formal parameters*)
     2.6              val (c, thy') =
     2.7 -              Sign.declare_const [] ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
     2.8 +              Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
     2.9              val cdef = cname ^ "_def"
    2.10              val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
    2.11              val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
     3.1 --- a/src/Pure/Isar/class.ML	Sun Oct 25 20:54:21 2009 +0100
     3.2 +++ b/src/Pure/Isar/class.ML	Sun Oct 25 21:35:46 2009 +0100
     3.3 @@ -237,7 +237,7 @@
     3.4          val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b;
     3.5        in
     3.6          thy
     3.7 -        |> Sign.declare_const [] ((b, ty0), syn)
     3.8 +        |> Sign.declare_const ((b, ty0), syn)
     3.9          |> snd
    3.10          |> pair ((Name.of_binding b, ty), (c, ty'))
    3.11        end;
     4.1 --- a/src/Pure/Isar/class_target.ML	Sun Oct 25 20:54:21 2009 +0100
     4.2 +++ b/src/Pure/Isar/class_target.ML	Sun Oct 25 21:35:46 2009 +0100
     4.3 @@ -21,10 +21,8 @@
     4.4  
     4.5    val begin: class list -> sort -> Proof.context -> Proof.context
     4.6    val init: class -> theory -> Proof.context
     4.7 -  val declare: class -> Properties.T
     4.8 -    -> (binding * mixfix) * term -> theory -> theory
     4.9 -  val abbrev: class -> Syntax.mode -> Properties.T
    4.10 -    -> (binding * mixfix) * term -> theory -> theory
    4.11 +  val declare: class -> (binding * mixfix) * term -> theory -> theory
    4.12 +  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
    4.13    val class_prefix: string -> string
    4.14    val refresh_syntax: class -> Proof.context -> Proof.context
    4.15    val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
    4.16 @@ -325,7 +323,7 @@
    4.17  
    4.18  val class_prefix = Logic.const_of_class o Long_Name.base_name;
    4.19  
    4.20 -fun declare class pos ((c, mx), dict) thy =
    4.21 +fun declare class ((c, mx), dict) thy =
    4.22    let
    4.23      val morph = morphism thy class;
    4.24      val b = Morphism.binding morph c;
    4.25 @@ -337,7 +335,7 @@
    4.26        |> map_types Type.strip_sorts;
    4.27    in
    4.28      thy
    4.29 -    |> Sign.declare_const pos ((b, Type.strip_sorts ty'), mx)
    4.30 +    |> Sign.declare_const ((b, Type.strip_sorts ty'), mx)
    4.31      |> snd
    4.32      |> Thm.add_def false false (b_def, def_eq)
    4.33      |>> Thm.varifyT
    4.34 @@ -347,7 +345,7 @@
    4.35      |> Sign.add_const_constraint (c', SOME ty')
    4.36    end;
    4.37  
    4.38 -fun abbrev class prmode pos ((c, mx), rhs) thy =
    4.39 +fun abbrev class prmode ((c, mx), rhs) thy =
    4.40    let
    4.41      val morph = morphism thy class;
    4.42      val unchecks = these_unchecks thy [class];
    4.43 @@ -358,7 +356,7 @@
    4.44      val rhs'' = map_types Logic.varifyT rhs';
    4.45    in
    4.46      thy
    4.47 -    |> Sign.add_abbrev (#1 prmode) pos (b, rhs'')
    4.48 +    |> Sign.add_abbrev (#1 prmode) (b, rhs'')
    4.49      |> snd
    4.50      |> Sign.add_const_constraint (c', SOME ty')
    4.51      |> Sign.notation true prmode [(Const (c', ty'), mx)]
     5.1 --- a/src/Pure/Isar/expression.ML	Sun Oct 25 20:54:21 2009 +0100
     5.2 +++ b/src/Pure/Isar/expression.ML	Sun Oct 25 21:35:46 2009 +0100
     5.3 @@ -639,7 +639,7 @@
     5.4      val ([pred_def], defs_thy) =
     5.5        thy
     5.6        |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
     5.7 -      |> Sign.declare_const [] ((bname, predT), NoSyn) |> snd
     5.8 +      |> Sign.declare_const ((bname, predT), NoSyn) |> snd
     5.9        |> PureThy.add_defs false
    5.10          [((Binding.map_name Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
    5.11      val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
     6.1 --- a/src/Pure/Isar/proof_context.ML	Sun Oct 25 20:54:21 2009 +0100
     6.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Oct 25 21:35:46 2009 +0100
     6.3 @@ -119,8 +119,7 @@
     6.4    val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     6.5      Context.generic -> Context.generic
     6.6    val add_const_constraint: string * typ option -> Proof.context -> Proof.context
     6.7 -  val add_abbrev: string -> Properties.T ->
     6.8 -    binding * term -> Proof.context -> (term * term) * Proof.context
     6.9 +  val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
    6.10    val revert_abbrev: string -> string -> Proof.context -> Proof.context
    6.11    val verbose: bool Unsynchronized.ref
    6.12    val setmp_verbose: ('a -> 'b) -> 'a -> 'b
    6.13 @@ -133,9 +132,6 @@
    6.14    val prems_limit: int Unsynchronized.ref
    6.15    val pretty_ctxt: Proof.context -> Pretty.T list
    6.16    val pretty_context: Proof.context -> Pretty.T list
    6.17 -  val query_type: Proof.context -> string -> Properties.T
    6.18 -  val query_const: Proof.context -> string -> Properties.T
    6.19 -  val query_class: Proof.context -> string -> Properties.T
    6.20  end;
    6.21  
    6.22  structure ProofContext: PROOF_CONTEXT =
    6.23 @@ -1051,13 +1047,13 @@
    6.24        in cert_term ctxt (Const (c, T)); T end;
    6.25    in ctxt |> (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end;
    6.26  
    6.27 -fun add_abbrev mode tags (b, raw_t) ctxt =
    6.28 +fun add_abbrev mode (b, raw_t) ctxt =
    6.29    let
    6.30      val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
    6.31        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
    6.32      val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
    6.33      val ((lhs, rhs), consts') = consts_of ctxt
    6.34 -      |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (b, t);
    6.35 +      |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode (b, t);
    6.36    in
    6.37      ctxt
    6.38      |> (map_consts o apfst) (K consts')
    6.39 @@ -1383,14 +1379,4 @@
    6.40      verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts)))
    6.41    end;
    6.42  
    6.43 -
    6.44 -(* query meta data *)
    6.45 -
    6.46 -val query_type = Type.the_tags o tsig_of;
    6.47 -
    6.48 -fun query_const ctxt name =
    6.49 -  Consts.the_tags (consts_of ctxt) name handle TYPE (msg, _, _) => error msg;
    6.50 -
    6.51 -fun query_class ctxt name = query_const ctxt (Logic.const_of_class name);
    6.52 -
    6.53  end;
     7.1 --- a/src/Pure/Isar/specification.ML	Sun Oct 25 20:54:21 2009 +0100
     7.2 +++ b/src/Pure/Isar/specification.ML	Sun Oct 25 21:35:46 2009 +0100
     7.3 @@ -161,7 +161,7 @@
     7.4      val xs = map (fn ((b, T), _) => (Name.of_binding b, T)) vars;
     7.5  
     7.6      (*consts*)
     7.7 -    val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
     7.8 +    val (consts, consts_thy) = thy |> fold_map Theory.specify_const vars;
     7.9      val subst = Term.subst_atomic (map Free xs ~~ consts);
    7.10  
    7.11      (*axioms*)
     8.1 --- a/src/Pure/Isar/theory_target.ML	Sun Oct 25 20:54:21 2009 +0100
     8.2 +++ b/src/Pure/Isar/theory_target.ML	Sun Oct 25 21:35:46 2009 +0100
     8.3 @@ -187,8 +187,8 @@
     8.4    in
     8.5      not (is_class andalso (similar_body orelse class_global)) ?
     8.6        (Context.mapping_result
     8.7 -        (Sign.add_abbrev PrintMode.internal [] arg)
     8.8 -        (ProofContext.add_abbrev PrintMode.internal [] arg)
     8.9 +        (Sign.add_abbrev PrintMode.internal arg)
    8.10 +        (ProofContext.add_abbrev PrintMode.internal arg)
    8.11        #-> (fn (lhs' as Const (d, _), _) =>
    8.12            similar_body ?
    8.13              (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
    8.14 @@ -214,13 +214,13 @@
    8.15                  if mx3 <> NoSyn then syntax_error c'
    8.16                  else LocalTheory.theory_result (Overloading.declare (c', U))
    8.17                    ##> Overloading.confirm b
    8.18 -            | NONE => LocalTheory.theory_result (Sign.declare_const [] ((b, U), mx3))));
    8.19 +            | NONE => LocalTheory.theory_result (Sign.declare_const ((b, U), mx3))));
    8.20      val (const, lthy') = lthy |> declare_const;
    8.21      val t = Term.list_comb (const, map Free xs);
    8.22    in
    8.23      lthy'
    8.24      |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default ((b, mx2), t))
    8.25 -    |> is_class ? class_target ta (Class_Target.declare target [] ((b, mx1), t))
    8.26 +    |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
    8.27      |> LocalDefs.add_def ((b, NoSyn), t)
    8.28    end;
    8.29  
    8.30 @@ -241,17 +241,17 @@
    8.31    in
    8.32      lthy |>
    8.33       (if is_locale then
    8.34 -        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal [] (b, global_rhs))
    8.35 +        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs))
    8.36          #-> (fn (lhs, _) =>
    8.37            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    8.38              term_syntax ta (locale_const ta prmode ((b, mx2), lhs')) #>
    8.39 -            is_class ? class_target ta (Class_Target.abbrev target prmode [] ((b, mx1), t'))
    8.40 +            is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t'))
    8.41            end)
    8.42        else
    8.43          LocalTheory.theory
    8.44 -          (Sign.add_abbrev (#1 prmode) [] (b, global_rhs) #-> (fn (lhs, _) =>
    8.45 +          (Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) =>
    8.46             Sign.notation true prmode [(lhs, mx3)])))
    8.47 -    |> ProofContext.add_abbrev PrintMode.internal [] (b, t) |> snd
    8.48 +    |> ProofContext.add_abbrev PrintMode.internal (b, t) |> snd
    8.49      |> LocalDefs.fixed_abbrev ((b, NoSyn), t)
    8.50    end;
    8.51  
     9.1 --- a/src/Pure/axclass.ML	Sun Oct 25 20:54:21 2009 +0100
     9.2 +++ b/src/Pure/axclass.ML	Sun Oct 25 21:35:46 2009 +0100
     9.3 @@ -305,7 +305,7 @@
     9.4    in
     9.5      thy
     9.6      |> Sign.mandatory_path name_inst
     9.7 -    |> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
     9.8 +    |> Sign.declare_const ((Binding.name c', T'), NoSyn)
     9.9      |-> (fn const' as Const (c'', _) =>
    9.10        Thm.add_def false true
    9.11          (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
    10.1 --- a/src/Pure/codegen.ML	Sun Oct 25 20:54:21 2009 +0100
    10.2 +++ b/src/Pure/codegen.ML	Sun Oct 25 21:35:46 2009 +0100
    10.3 @@ -337,7 +337,7 @@
    10.4      val tc = Sign.intern_type thy s;
    10.5    in
    10.6      case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of
    10.7 -      SOME (Type.LogicalType i, _) =>
    10.8 +      SOME (Type.LogicalType i) =>
    10.9          if num_args_of (fst syn) > i then
   10.10            error ("More arguments than corresponding type constructor " ^ s)
   10.11          else
    11.1 --- a/src/Pure/consts.ML	Sun Oct 25 20:54:21 2009 +0100
    11.2 +++ b/src/Pure/consts.ML	Sun Oct 25 21:35:46 2009 +0100
    11.3 @@ -16,7 +16,6 @@
    11.4    val the_type: T -> string -> typ                             (*exception TYPE*)
    11.5    val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
    11.6    val type_scheme: T -> string -> typ                          (*exception TYPE*)
    11.7 -  val the_tags: T -> string -> Properties.T                    (*exception TYPE*)
    11.8    val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
    11.9    val the_constraint: T -> string -> typ                       (*exception TYPE*)
   11.10    val space_of: T -> Name_Space.T
   11.11 @@ -30,9 +29,9 @@
   11.12    val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   11.13    val typargs: T -> string * typ -> typ list
   11.14    val instance: T -> string * typ list -> typ
   11.15 -  val declare: bool -> Name_Space.naming -> Properties.T -> binding * typ -> T -> T
   11.16 +  val declare: bool -> Name_Space.naming -> binding * typ -> T -> T
   11.17    val constrain: string * typ option -> T -> T
   11.18 -  val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string -> Properties.T ->
   11.19 +  val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string ->
   11.20      binding * term -> T -> (term * term) * T
   11.21    val revert_abbrev: string -> string -> T -> T
   11.22    val hide: bool -> string -> T -> T
   11.23 @@ -47,7 +46,7 @@
   11.24  
   11.25  (* datatype T *)
   11.26  
   11.27 -type decl = {T: typ, typargs: int list list, tags: Properties.T, authentic: bool};
   11.28 +type decl = {T: typ, typargs: int list list, authentic: bool};
   11.29  type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
   11.30  
   11.31  datatype T = Consts of
   11.32 @@ -71,7 +70,8 @@
   11.33  
   11.34  (* reverted abbrevs *)
   11.35  
   11.36 -val empty_abbrevs = Item_Net.init (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u') #1;
   11.37 +val empty_abbrevs =
   11.38 +  Item_Net.init (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u') #1;
   11.39  
   11.40  fun insert_abbrevs mode abbrs =
   11.41    Symtab.map_default (mode, empty_abbrevs) (Item_Net.insert abbrs);
   11.42 @@ -110,7 +110,6 @@
   11.43  val the_decl = #1 oo the_const;
   11.44  val type_scheme = #T oo the_decl;
   11.45  val type_arguments = #typargs oo the_decl;
   11.46 -val the_tags = #tags oo the_decl;
   11.47  
   11.48  val is_monomorphic = null oo type_arguments;
   11.49  
   11.50 @@ -232,10 +231,10 @@
   11.51  
   11.52  (* declarations *)
   11.53  
   11.54 -fun declare authentic naming tags (b, declT) =
   11.55 +fun declare authentic naming (b, declT) =
   11.56    map_consts (fn (decls, constraints, rev_abbrevs) =>
   11.57      let
   11.58 -      val decl = {T = declT, typargs = typargs_of declT, tags = tags, authentic = authentic};
   11.59 +      val decl = {T = declT, typargs = typargs_of declT, authentic = authentic};
   11.60        val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
   11.61      in (decls', constraints, rev_abbrevs) end);
   11.62  
   11.63 @@ -267,7 +266,7 @@
   11.64  
   11.65  in
   11.66  
   11.67 -fun abbreviate pp tsig naming mode tags (b, raw_rhs) consts =
   11.68 +fun abbreviate pp tsig naming mode (b, raw_rhs) consts =
   11.69    let
   11.70      val cert_term = certify pp tsig false consts;
   11.71      val expand_term = certify pp tsig true consts;
   11.72 @@ -286,7 +285,7 @@
   11.73    in
   11.74      consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
   11.75        let
   11.76 -        val decl = {T = T, typargs = typargs_of T, tags = tags, authentic = true};
   11.77 +        val decl = {T = T, typargs = typargs_of T, authentic = true};
   11.78          val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
   11.79          val (_, decls') = decls
   11.80            |> Name_Space.define true naming (b, (decl, SOME abbr));
    12.1 --- a/src/Pure/display.ML	Sun Oct 25 20:54:21 2009 +0100
    12.2 +++ b/src/Pure/display.ML	Sun Oct 25 21:35:46 2009 +0100
    12.3 @@ -146,14 +146,14 @@
    12.4        [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
    12.5  
    12.6      val tfrees = map (fn v => TFree (v, []));
    12.7 -    fun pretty_type syn (t, (Type.LogicalType n, _)) =
    12.8 +    fun pretty_type syn (t, (Type.LogicalType n)) =
    12.9            if syn then NONE
   12.10            else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
   12.11 -      | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
   12.12 +      | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'))) =
   12.13            if syn <> syn' then NONE
   12.14            else SOME (Pretty.block
   12.15              [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
   12.16 -      | pretty_type syn (t, (Type.Nonterminal, _)) =
   12.17 +      | pretty_type syn (t, Type.Nonterminal) =
   12.18            if not syn then NONE
   12.19            else SOME (prt_typ (Type (t, [])));
   12.20  
    13.1 --- a/src/Pure/sign.ML	Sun Oct 25 20:54:21 2009 +0100
    13.2 +++ b/src/Pure/sign.ML	Sun Oct 25 21:35:46 2009 +0100
    13.3 @@ -90,10 +90,10 @@
    13.4    val del_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
    13.5    val del_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
    13.6    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
    13.7 -  val declare_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
    13.8 +  val declare_const: (binding * typ) * mixfix -> theory -> term * theory
    13.9    val add_consts: (binding * string * mixfix) list -> theory -> theory
   13.10    val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
   13.11 -  val add_abbrev: string -> Properties.T -> binding * term -> theory -> (term * term) * theory
   13.12 +  val add_abbrev: string -> binding * term -> theory -> (term * term) * theory
   13.13    val revert_abbrev: string -> string -> theory -> theory
   13.14    val add_const_constraint: string * typ option -> theory -> theory
   13.15    val primitive_class: binding * class list -> theory -> theory
   13.16 @@ -434,7 +434,7 @@
   13.17    let
   13.18      val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Name.of_binding a, n, mx)) types) syn;
   13.19      val decls = map (fn (a, n, mx) => (Binding.map_name (Syntax.type_name mx) a, n)) types;
   13.20 -    val tsig' = fold (Type.add_type naming []) decls tsig;
   13.21 +    val tsig' = fold (Type.add_type naming) decls tsig;
   13.22    in (naming, syn', tsig', consts) end);
   13.23  
   13.24  
   13.25 @@ -443,7 +443,7 @@
   13.26  fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   13.27    let
   13.28      val syn' = Syntax.update_consts (map Name.of_binding ns) syn;
   13.29 -    val tsig' = fold (Type.add_nonterminal naming []) ns tsig;
   13.30 +    val tsig' = fold (Type.add_nonterminal naming) ns tsig;
   13.31    in (naming, syn', tsig', consts) end);
   13.32  
   13.33  
   13.34 @@ -457,7 +457,7 @@
   13.35        val b = Binding.map_name (Syntax.type_name mx) a;
   13.36        val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
   13.37          handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
   13.38 -      val tsig' = Type.add_abbrev naming [] abbr tsig;
   13.39 +      val tsig' = Type.add_abbrev naming abbr tsig;
   13.40      in (naming, syn', tsig', consts) end);
   13.41  
   13.42  val add_tyabbrs = fold (gen_add_tyabbr Syntax.parse_typ);
   13.43 @@ -495,7 +495,7 @@
   13.44  
   13.45  local
   13.46  
   13.47 -fun gen_add_consts parse_typ authentic tags raw_args thy =
   13.48 +fun gen_add_consts parse_typ authentic raw_args thy =
   13.49    let
   13.50      val ctxt = ProofContext.init thy;
   13.51      val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
   13.52 @@ -512,20 +512,20 @@
   13.53      val args = map prep raw_args;
   13.54    in
   13.55      thy
   13.56 -    |> map_consts (fold (Consts.declare authentic (naming_of thy) tags o #1) args)
   13.57 +    |> map_consts (fold (Consts.declare authentic (naming_of thy) o #1) args)
   13.58      |> add_syntax_i (map #2 args)
   13.59      |> pair (map #3 args)
   13.60    end;
   13.61  
   13.62  in
   13.63  
   13.64 -fun add_consts args = snd o gen_add_consts Syntax.parse_typ false [] args;
   13.65 -fun add_consts_i args = snd o gen_add_consts (K I) false [] args;
   13.66 +fun add_consts args = snd o gen_add_consts Syntax.parse_typ false args;
   13.67 +fun add_consts_i args = snd o gen_add_consts (K I) false args;
   13.68  
   13.69 -fun declare_const tags ((b, T), mx) thy =
   13.70 +fun declare_const ((b, T), mx) thy =
   13.71    let
   13.72      val pos = Binding.pos_of b;
   13.73 -    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags [(b, T, mx)] thy;
   13.74 +    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true [(b, T, mx)] thy;
   13.75      val _ = Position.report (Markup.const_decl c) pos;
   13.76    in (const, thy') end;
   13.77  
   13.78 @@ -534,14 +534,14 @@
   13.79  
   13.80  (* abbreviations *)
   13.81  
   13.82 -fun add_abbrev mode tags (b, raw_t) thy =
   13.83 +fun add_abbrev mode (b, raw_t) thy =
   13.84    let
   13.85      val pp = Syntax.pp_global thy;
   13.86      val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
   13.87      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
   13.88        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
   13.89      val (res, consts') = consts_of thy
   13.90 -      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (b, t);
   13.91 +      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode (b, t);
   13.92    in (res, thy |> map_consts (K consts')) end;
   13.93  
   13.94  fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);
    14.1 --- a/src/Pure/theory.ML	Sun Oct 25 20:54:21 2009 +0100
    14.2 +++ b/src/Pure/theory.ML	Sun Oct 25 21:35:46 2009 +0100
    14.3 @@ -35,7 +35,7 @@
    14.4    val add_defs: bool -> bool -> (binding * string) list -> theory -> theory
    14.5    val add_finals_i: bool -> term list -> theory -> theory
    14.6    val add_finals: bool -> string list -> theory -> theory
    14.7 -  val specify_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
    14.8 +  val specify_const: (binding * typ) * mixfix -> theory -> term * theory
    14.9  end
   14.10  
   14.11  structure Theory: THEORY =
   14.12 @@ -219,8 +219,8 @@
   14.13      val name = if a = "" then (#1 lhs ^ " axiom") else a;
   14.14    in thy |> map_defs (dependencies thy false false name lhs rhs) end;
   14.15  
   14.16 -fun specify_const tags decl thy =
   14.17 -  let val (t as Const const, thy') = Sign.declare_const tags decl thy
   14.18 +fun specify_const decl thy =
   14.19 +  let val (t as Const const, thy') = Sign.declare_const decl thy
   14.20    in (t, add_deps "" const [] thy') end;
   14.21  
   14.22  
    15.1 --- a/src/Pure/type.ML	Sun Oct 25 20:54:21 2009 +0100
    15.2 +++ b/src/Pure/type.ML	Sun Oct 25 21:35:46 2009 +0100
    15.3 @@ -16,7 +16,7 @@
    15.4    val rep_tsig: tsig ->
    15.5     {classes: Name_Space.T * Sorts.algebra,
    15.6      default: sort,
    15.7 -    types: (decl * Properties.T) Name_Space.table,
    15.8 +    types: decl Name_Space.table,
    15.9      log_types: string list}
   15.10    val empty_tsig: tsig
   15.11    val defaultS: tsig -> sort
   15.12 @@ -39,7 +39,6 @@
   15.13    val cert_typ: tsig -> typ -> typ
   15.14    val arity_number: tsig -> string -> int
   15.15    val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
   15.16 -  val the_tags: tsig -> string -> Properties.T
   15.17  
   15.18    (*special treatment of type vars*)
   15.19    val strip_sorts: typ -> typ
   15.20 @@ -73,9 +72,9 @@
   15.21    val add_class: Pretty.pp -> Name_Space.naming -> binding * class list -> tsig -> tsig
   15.22    val hide_class: bool -> string -> tsig -> tsig
   15.23    val set_defsort: sort -> tsig -> tsig
   15.24 -  val add_type: Name_Space.naming -> Properties.T -> binding * int -> tsig -> tsig
   15.25 -  val add_abbrev: Name_Space.naming -> Properties.T -> binding * string list * typ -> tsig -> tsig
   15.26 -  val add_nonterminal: Name_Space.naming -> Properties.T -> binding -> tsig -> tsig
   15.27 +  val add_type: Name_Space.naming -> binding * int -> tsig -> tsig
   15.28 +  val add_abbrev: Name_Space.naming -> binding * string list * typ -> tsig -> tsig
   15.29 +  val add_nonterminal: Name_Space.naming -> binding -> tsig -> tsig
   15.30    val hide_type: bool -> string -> tsig -> tsig
   15.31    val add_arity: Pretty.pp -> arity -> tsig -> tsig
   15.32    val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
   15.33 @@ -101,7 +100,7 @@
   15.34    TSig of {
   15.35      classes: Name_Space.T * Sorts.algebra,  (*order-sorted algebra of type classes*)
   15.36      default: sort,                          (*default sort on input*)
   15.37 -    types: (decl * Properties.T) Name_Space.table,  (*declared types*)
   15.38 +    types: decl Name_Space.table,           (*declared types*)
   15.39      log_types: string list};                (*logical types sorted by number of arguments*)
   15.40  
   15.41  fun rep_tsig (TSig comps) = comps;
   15.42 @@ -112,7 +111,7 @@
   15.43  fun build_tsig (classes, default, types) =
   15.44    let
   15.45      val log_types =
   15.46 -      Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (snd types) []
   15.47 +      Symtab.fold (fn (c, LogicalType n) => cons (c, n) | _ => I) (snd types) []
   15.48        |> Library.sort (int_ord o pairself snd) |> map fst;
   15.49    in make_tsig (classes, default, types, log_types) end;
   15.50  
   15.51 @@ -165,11 +164,6 @@
   15.52  
   15.53  fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
   15.54  
   15.55 -fun the_tags tsig c =
   15.56 -  (case lookup_type tsig c of
   15.57 -    SOME (_, tags) => tags
   15.58 -  | NONE => error (undecl_type c));
   15.59 -
   15.60  
   15.61  (* certified types *)
   15.62  
   15.63 @@ -197,13 +191,13 @@
   15.64              fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
   15.65            in
   15.66              (case lookup_type tsig c of
   15.67 -              SOME (LogicalType n, _) => (nargs n; Type (c, Ts'))
   15.68 -            | SOME (Abbreviation (vs, U, syn), _) =>
   15.69 +              SOME (LogicalType n) => (nargs n; Type (c, Ts'))
   15.70 +            | SOME (Abbreviation (vs, U, syn)) =>
   15.71                 (nargs (length vs);
   15.72                  if syn then check_logical c else ();
   15.73                  if normalize then inst_typ (vs ~~ Ts') U
   15.74                  else Type (c, Ts'))
   15.75 -            | SOME (Nonterminal, _) => (nargs 0; check_logical c; T)
   15.76 +            | SOME Nonterminal => (nargs 0; check_logical c; T)
   15.77              | NONE => err (undecl_type c))
   15.78            end
   15.79        | cert (TFree (x, S)) = TFree (x, cert_sort tsig S)
   15.80 @@ -224,7 +218,7 @@
   15.81  
   15.82  fun arity_number tsig a =
   15.83    (case lookup_type tsig a of
   15.84 -    SOME (LogicalType n, _) => n
   15.85 +    SOME (LogicalType n) => n
   15.86    | _ => error (undecl_type a));
   15.87  
   15.88  fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
   15.89 @@ -525,7 +519,7 @@
   15.90    let
   15.91      val _ =
   15.92        (case lookup_type tsig t of
   15.93 -        SOME (LogicalType n, _) => if length Ss <> n then error (bad_nargs t) else ()
   15.94 +        SOME (LogicalType n) => if length Ss <> n then error (bad_nargs t) else ()
   15.95        | SOME _ => error ("Logical type constructor expected: " ^ quote t)
   15.96        | NONE => error (undecl_type t));
   15.97      val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
   15.98 @@ -555,8 +549,8 @@
   15.99  
  15.100  local
  15.101  
  15.102 -fun new_decl naming tags (c, decl) types =
  15.103 -  #2 (Name_Space.define true naming (c, (decl, tags)) types);
  15.104 +fun new_decl naming (c, decl) types =
  15.105 +  #2 (Name_Space.define true naming (c, decl) types);
  15.106  
  15.107  fun map_types f = map_tsig (fn (classes, default, types) =>
  15.108    let
  15.109 @@ -566,20 +560,21 @@
  15.110    in (classes, default, (space', tab')) end);
  15.111  
  15.112  fun syntactic types (Type (c, Ts)) =
  15.113 -      (case Symtab.lookup types c of SOME (Nonterminal, _) => true | _ => false)
  15.114 +      (case Symtab.lookup types c of SOME Nonterminal => true | _ => false)
  15.115          orelse exists (syntactic types) Ts
  15.116    | syntactic _ _ = false;
  15.117  
  15.118  in
  15.119  
  15.120 -fun add_type naming tags (c, n) =
  15.121 +fun add_type naming (c, n) =
  15.122    if n < 0 then error ("Bad type constructor declaration " ^ quote (Binding.str_of c))
  15.123 -  else map_types (new_decl naming tags (c, LogicalType n));
  15.124 +  else map_types (new_decl naming (c, LogicalType n));
  15.125  
  15.126 -fun add_abbrev naming tags (a, vs, rhs) tsig = tsig |> map_types (fn types =>
  15.127 +fun add_abbrev naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
  15.128    let
  15.129      fun err msg =
  15.130 -      cat_error msg ("The error(s) above occurred in type abbreviation " ^ quote (Binding.str_of a));
  15.131 +      cat_error msg ("The error(s) above occurred in type abbreviation " ^
  15.132 +        quote (Binding.str_of a));
  15.133      val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs))
  15.134        handle TYPE (msg, _, _) => err msg;
  15.135      val _ =
  15.136 @@ -590,9 +585,9 @@
  15.137        (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
  15.138          [] => []
  15.139        | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
  15.140 -  in types |> new_decl naming tags (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
  15.141 +  in types |> new_decl naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
  15.142  
  15.143 -fun add_nonterminal naming tags = map_types o new_decl naming tags o rpair Nonterminal;
  15.144 +fun add_nonterminal naming = map_types o new_decl naming o rpair Nonterminal;
  15.145  
  15.146  end;
  15.147