--- a/src/Pure/sign.ML Wed Apr 28 10:51:34 2010 +0200
+++ b/src/Pure/sign.ML Wed Apr 28 11:09:19 2010 +0200
@@ -25,6 +25,7 @@
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
@@ -68,8 +69,6 @@
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
@@ -198,6 +197,7 @@
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;
@@ -334,15 +334,6 @@
(** 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) =>