renamed Defs.node to Defs.item;
clarified type Defs.item;
clarified item_ord for printing;

--- a/src/Pure/defs.ML	Tue Sep 22 16:17:49 2015 +0200
+++ b/src/Pure/defs.ML	Tue Sep 22 16:49:56 2015 +0200
@@ -7,9 +7,10 @@
 
 signature DEFS =
 sig
-  datatype node = NConst of string | NType of string
-  val fast_node_ord: node * node -> order
-  val pretty_node: Proof.context -> node * typ list -> Pretty.T
+  datatype item_kind = Constant | Type
+  type item = item_kind * string
+  val item_ord: item * item -> order
+  val pretty_item: Proof.context -> item * typ list -> Pretty.T
   val plain_args: typ list -> bool
   type T
   type spec =
@@ -17,44 +18,49 @@
     description: string,
     pos: Position.T,
     lhs: typ list,
-    rhs: (node * typ list) list}
-  val all_specifications_of: T -> (node * spec list) list
-  val specifications_of: T -> node -> spec list
+    rhs: (item * typ list) list}
+  val all_specifications_of: T -> (item * spec list) list
+  val specifications_of: T -> item -> spec list
   val dest: T ->
-   {restricts: ((node * typ list) * string) list,
-    reducts: ((node * typ list) * (node * typ list) list) list}
+   {restricts: ((item * typ list) * string) list,
+    reducts: ((item * typ list) * (item * typ list) list) list}
   val empty: T
   val merge: Proof.context -> T * T -> T
   val define: Proof.context -> bool -> string option -> string ->
-    node * typ list -> (node * typ list) list -> T -> T
-end
-
+    item * typ list -> (item * typ list) list -> T -> T
+end;
 
 structure Defs: DEFS =
 struct
 
-datatype node = NConst of string | NType of string
+(* specification items *)
+
+datatype item_kind = Constant | Type;
+type item = item_kind * string;
+
+fun item_kind_ord (Constant, Type) = LESS
+  | item_kind_ord (Type, Constant) = GREATER
+  | item_kind_ord _ = EQUAL;
 
-fun fast_node_ord (NConst s1, NConst s2) = fast_string_ord (s1, s2)
-  | fast_node_ord (NType s1, NType s2) = fast_string_ord (s1, s2)
-  | fast_node_ord (NConst _, NType _) = LESS
-  | fast_node_ord (NType _, NConst _) = GREATER
+val item_ord = prod_ord item_kind_ord string_ord;
+val fast_item_ord = prod_ord item_kind_ord fast_string_ord;
 
-fun string_of_node (NConst s) = "constant " ^ s
-  | string_of_node (NType s) = "type " ^ s
+val print_item_kind = fn Constant => "constant" | Type => "type";
+fun print_item (k, s) = print_item_kind k ^ " " ^ quote s;
 
-structure Deftab = Table(type key = node val ord = fast_node_ord);
+structure Itemtab = Table(type key = item val ord = fast_item_ord);
+
 
 (* type arguments *)
 
 type args = typ list;
 
-fun pretty_node ctxt (c, args) =
+fun pretty_item ctxt (c, args) =
   let
     val prt_args =
       if null args then []
       else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)];
-  in Pretty.block (Pretty.str (string_of_node c) :: prt_args) end;
+  in Pretty.block (Pretty.str (print_item c) :: prt_args) end;
 
 fun plain_args args =
   forall Term.is_TVar args andalso not (has_duplicates (op =) args);
@@ -78,31 +84,31 @@
   description: string,
   pos: Position.T,
   lhs: args,
-  rhs: (node * args) list};
+  rhs: (item * args) list};
 
 type def =
  {specs: spec Inttab.table,  (*source specifications*)
   restricts: (args * string) list,  (*global restrictions imposed by incomplete patterns*)
-  reducts: (args * (node * args) list) list};  (*specifications as reduction system*)
+  reducts: (args * (item * args) list) list};  (*specifications as reduction system*)
 
 fun make_def (specs, restricts, reducts) =
   {specs = specs, restricts = restricts, reducts = reducts}: def;
 
 fun map_def c f =
-  Deftab.default (c, make_def (Inttab.empty, [], [])) #>
-  Deftab.map_entry c (fn {specs, restricts, reducts}: def =>
+  Itemtab.default (c, make_def (Inttab.empty, [], [])) #>
+  Itemtab.map_entry c (fn {specs, restricts, reducts}: def =>
     make_def (f (specs, restricts, reducts)));
 
 
-datatype T = Defs of def Deftab.table;
+datatype T = Defs of def Itemtab.table;
 
 fun lookup_list which defs c =
-  (case Deftab.lookup defs c of
+  (case Itemtab.lookup defs c of
     SOME (def: def) => which def
   | NONE => []);
 
 fun all_specifications_of (Defs defs) =
-  (map o apsnd) (map snd o Inttab.dest o #specs) (Deftab.dest defs);
+  (map o apsnd) (map snd o Inttab.dest o #specs) (Itemtab.dest defs);
 
 fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs;
 
@@ -111,13 +117,13 @@
 
 fun dest (Defs defs) =
   let
-    val restricts = Deftab.fold (fn (c, {restricts, ...}) =>
+    val restricts = Itemtab.fold (fn (c, {restricts, ...}) =>
       fold (fn (args, description) => cons ((c, args), description)) restricts) defs [];
-    val reducts = Deftab.fold (fn (c, {reducts, ...}) =>
+    val reducts = Itemtab.fold (fn (c, {reducts, ...}) =>
       fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs [];
   in {restricts = restricts, reducts = reducts} end;
 
-val empty = Defs Deftab.empty;
+val empty = Defs Itemtab.empty;
 
 
 (* specifications *)
@@ -125,7 +131,7 @@
 fun disjoint_specs c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) =
   Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) =>
     i = j orelse disjoint_args (Ts, Us) orelse
-      error ("Clash of specifications for " ^ quote (string_of_node c) ^ ":\n" ^
+      error ("Clash of specifications for " ^ print_item c ^ ":\n" ^
         "  " ^ quote a ^ Position.here pos_a ^ "\n" ^
         "  " ^ quote b ^ Position.here pos_b));
 
@@ -143,7 +149,7 @@
 
 local
 
-val prt = Pretty.string_of oo pretty_node;
+val prt = Pretty.string_of oo pretty_item;
 fun err ctxt (c, args) (d, Us) s1 s2 =
   error (s1 ^ " dependency of " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2);
 
@@ -189,12 +195,12 @@
         else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))
       end;
     fun norm_all defs =
-      (case Deftab.fold norm_update defs (false, defs) of
+      (case Itemtab.fold norm_update defs (false, defs) of
         (true, defs') => norm_all defs'
       | (false, _) => defs);
     fun check defs (c, {reducts, ...}: def) =
       reducts |> forall (fn (args, deps) => forall (wellformed ctxt defs (c, args)) deps);
-  in norm_all #> (fn defs => tap (Deftab.forall (check defs)) defs) end;
+  in norm_all #> (fn defs => tap (Itemtab.forall (check defs)) defs) end;
 
 fun dependencies ctxt (c, args) restr deps =
   map_def c (fn (specs, restricts, reducts) =>
@@ -217,8 +223,8 @@
     fun add_def (c, {restricts, reducts, ...}: def) =
       fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
   in
-    Defs (Deftab.join join_specs (defs1, defs2)
-      |> normalize ctxt |> Deftab.fold add_def defs2)
+    Defs (Itemtab.join join_specs (defs1, defs2)
+      |> normalize ctxt |> Itemtab.fold add_def defs2)
   end;
 
 
@@ -229,7 +235,7 @@
     val pos = Position.thread_data ();
     val restr =
       if plain_args args orelse
-        (case args of [Type (_, rec_args)] => plain_args rec_args | _ => false)
+        (case args of [Term.Type (_, rec_args)] => plain_args rec_args | _ => false)
       then [] else [(args, description)];
     val spec =
       (serial (), {def = def, description = description, pos = pos, lhs = args, rhs = deps});

--- a/src/Pure/display.ML	Tue Sep 22 16:17:49 2015 +0200
+++ b/src/Pure/display.ML	Tue Sep 22 16:49:56 2015 +0200
@@ -104,8 +104,8 @@
     fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
     val prt_term_no_vars = prt_term o Logic.unvarify_global;
     fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
-    val prt_node = Defs.pretty_node ctxt;
-    fun sort_node_wrt f = sort (Defs.fast_node_ord o apply2 f)
+    val prt_item = Defs.pretty_item ctxt;
+    fun sort_item_by f = sort (Defs.item_ord o apply2 f);
 
     fun pretty_classrel (c, []) = prt_cls c
       | pretty_classrel (c, cs) = Pretty.block
@@ -135,14 +135,14 @@
       Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t];
 
     fun pretty_finals reds = Pretty.block
-      (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_node o fst) reds));
+      (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_item o fst) reds));
 
     fun pretty_reduct (lhs, rhs) = Pretty.block
-      ([prt_node lhs, Pretty.str "  ->", Pretty.brk 2] @
-        Pretty.commas (map prt_node ((sort_node_wrt #1) rhs)));
+      ([prt_item lhs, Pretty.str "  ->", Pretty.brk 2] @
+        Pretty.commas (map prt_item (sort_item_by #1 rhs)));
 
     fun pretty_restrict (const, name) =
-      Pretty.block ([prt_node const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
+      Pretty.block ([prt_item const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
 
     val defs = Theory.defs_of thy;
     val {restricts, reducts} = Defs.dest defs;
@@ -155,8 +155,11 @@
     val classes = Sorts.classes_of class_algebra;
     val arities = Sorts.arities_of class_algebra;
 
-    fun extern_node (Defs.NConst c) = Defs.NConst (Name_Space.extern ctxt const_space c)
-      | extern_node (Defs.NType t) = Defs.NType (Name_Space.extern ctxt type_space t);
+    fun extern_item (Defs.Constant, c) = (Defs.Constant, Name_Space.extern ctxt const_space c)
+      | extern_item (Defs.Type, c) = (Defs.Type, Name_Space.extern ctxt type_space c);
+
+    fun prune_item (Defs.Constant, c) = not verbose andalso Consts.is_concealed consts c
+      | prune_item (Defs.Type, c) = not verbose andalso Name_Space.is_concealed type_space c;
 
     val clsses =
       Name_Space.extern_entries verbose ctxt class_space
@@ -167,11 +170,6 @@
       Name_Space.extern_entries verbose ctxt (Type.type_space tsig) (Symtab.dest arities)
       |> map (apfst #1);
 
-    fun prune_const c = not verbose andalso Consts.is_concealed consts c;
-
-    fun prune_node (Defs.NConst c) = prune_const c
-      | prune_node (Defs.NType t) = not verbose andalso Name_Space.is_concealed type_space t;
-
     val cnsts = Name_Space.markup_entries verbose ctxt const_space constants;
     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
@@ -179,13 +177,13 @@
 
     val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy);
 
-    val (reds0, (reds1, reds2)) = filter_out (prune_node o fst o fst) reducts
+    val (reds0, (reds1, reds2)) = filter_out (prune_item o fst o fst) reducts
       |> map (fn (lhs, rhs) =>
-        (apfst extern_node lhs, map (apfst extern_node) (filter_out (prune_node o fst) rhs)))
-      |> sort_node_wrt (#1 o #1)
+        (apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs)))
+      |> sort_item_by (#1 o #1)
       |> List.partition (null o #2)
       ||> List.partition (Defs.plain_args o #2 o #1);
-    val rests = restricts |> map (apfst (apfst extern_node)) |> sort_node_wrt (#1 o #1);
+    val rests = restricts |> map (apfst (apfst extern_item)) |> sort_item_by (#1 o #1);
   in
     [Pretty.strs ("names:" :: Context.display_names thy)] @
     [Pretty.big_list "classes:" (map pretty_classrel clsses),

--- a/src/Pure/theory.ML	Tue Sep 22 16:17:49 2015 +0200
+++ b/src/Pure/theory.ML	Tue Sep 22 16:49:56 2015 +0200
@@ -221,14 +221,17 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val consts = Sign.consts_of thy;
+
     fun prep (DConst const) =
-      let val Const (c, T) = Sign.no_vars ctxt (Const const)
-      in (Defs.NConst c, Consts.typargs consts (c, Logic.varifyT_global T)) end
+        let val Const (c, T) = Sign.no_vars ctxt (Const const)
+        in ((Defs.Constant, c), Consts.typargs consts (c, Logic.varifyT_global T)) end
     | prep (DType typ) =
-      let val Type (c, T) = Type.no_tvars (Type typ)
-      in (Defs.NType c, map Logic.varifyT_global T) end;
+        let val Type (c, Ts) = Type.no_tvars (Type typ)
+        in ((Defs.Type, c), map Logic.varifyT_global Ts) end;
+
     fun fold_dep_tfree f (DConst (_, T)) = fold_atyps (fn TFree v => f v | _ => I) T
-      | fold_dep_tfree f (DType (_, Ts)) = fold (fold_atyps (fn TFree v => f v | _ => I)) Ts
+      | fold_dep_tfree f (DType (_, Ts)) = fold (fold_atyps (fn TFree v => f v | _ => I)) Ts;
+
     val lhs_vars = fold_dep_tfree (insert (op =)) lhs [];
     val rhs_extras = fold (fold_dep_tfree
       (fn v => if member (op =) lhs_vars v then I else insert (op =) v)) rhs [];