src/Pure/defs.ML

 signature DEFS =
 sig
   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 pretty_args: Proof.context -> typ list -> Pretty.T list
   val plain_args: typ list -> bool
   type T
   type spec =
    {def: string option,
     description: string,

   | item_kind_ord _ = EQUAL;
 
 val item_ord = prod_ord item_kind_ord string_ord;
 val fast_item_ord = prod_ord item_kind_ord fast_string_ord;
 
-val print_item_kind = fn Constant => "constant" | Type => "type";
-fun print_item (k, s) = print_item_kind k ^ " " ^ quote s;
+fun print_item (k, s) = if k = Constant then s else "type " ^ s;
 
 structure Itemtab = Table(type key = item val ord = fast_item_ord);
 
 
 (* type arguments *)
 
 type args = typ list;
 
-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 (print_item c) :: prt_args) end;
+fun pretty_args ctxt args =
+  if null args then []
+  else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)];
+
+fun pretty_entry ctxt (c, args) =
+  Pretty.block (Pretty.str (print_item c) :: pretty_args ctxt args);
 
 fun plain_args args =
   forall Term.is_TVar args andalso not (has_duplicates (op =) args);
 
 fun disjoint_args (Ts, Us) =

 
 (* normalized dependencies: reduction with well-formedness check *)
 
 local
 
-val prt = Pretty.string_of oo pretty_item;
+val prt = Pretty.string_of oo pretty_entry;
 fun err ctxt (c, args) (d, Us) s1 s2 =
   error (s1 ^ " dependency of " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2);
 
 fun acyclic ctxt (c, args) (d, Us) =
   c <> d orelse