src/Pure/sign.ML

   val classes_of: theory -> Sorts.algebra
   val all_classes: theory -> class list
   val super_classes: theory -> class -> class list
   val minimize_sort: theory -> sort -> sort
   val complete_sort: theory -> sort -> sort
+  val set_defsort: sort -> theory -> theory
   val defaultS: theory -> sort
   val subsort: theory -> sort * sort -> bool
   val of_sort: theory -> typ * sort -> bool
   val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list
   val is_logtype: theory -> string -> bool

   val certify_term: theory -> term -> term * typ * int
   val cert_term: theory -> term -> term
   val cert_prop: theory -> term -> term
   val no_frees: Pretty.pp -> term -> term
   val no_vars: Pretty.pp -> term -> term
-  val add_defsort: string -> theory -> theory
-  val add_defsort_i: sort -> theory -> theory
   val add_types: (binding * int * mixfix) list -> theory -> theory
   val add_nonterminals: binding list -> theory -> theory
   val add_type_abbrev: binding * string list * typ -> theory -> theory
   val add_syntax: (string * string * mixfix) list -> theory -> theory
   val add_syntax_i: (string * typ * mixfix) list -> theory -> theory

 val all_classes = Sorts.all_classes o classes_of;
 val super_classes = Sorts.super_classes o classes_of;
 val minimize_sort = Sorts.minimize_sort o classes_of;
 val complete_sort = Sorts.complete_sort o classes_of;
 
+val set_defsort = map_tsig o Type.set_defsort;
 val defaultS = Type.defaultS o tsig_of;
 val subsort = Type.subsort o tsig_of;
 val of_sort = Type.of_sort o tsig_of;
 val witness_sorts = Type.witness_sorts o tsig_of;
 val is_logtype = member (op =) o Type.logical_types o tsig_of;

 val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar;
 
 
 
 (** signature extension functions **)  (*exception ERROR/TYPE*)
-
-(* add default sort *)
-
-fun gen_add_defsort prep_sort s thy =
-  thy |> map_tsig (Type.set_defsort (prep_sort thy s));
-
-val add_defsort = gen_add_defsort Syntax.read_sort_global;
-val add_defsort_i = gen_add_defsort certify_sort;
-
 
 (* add type constructors *)
 
 fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   let