# HG changeset patch
# User wenzelm
# Date 1272445759 -7200
# Node ID 78721f3adb13916188b14e9fd5b6e50536e4a714
# Parent  edb757388592a3910464ee1ed6fcc3de27e01d9f
modernized/simplified Sign.set_defsort;

diff -r edb757388592 -r 78721f3adb13 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Apr 28 10:51:34 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 28 11:09:19 2010 +0200
@@ -97,7 +97,8 @@
 
 val _ =
   OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
-    (P.sort >> (Toplevel.theory o Sign.add_defsort));
+    (P.sort >>
+      (fn s => Toplevel.theory (fn thy => Sign.set_defsort (Syntax.read_sort_global thy s) thy)));
 
 
 (* types *)
diff -r edb757388592 -r 78721f3adb13 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Wed Apr 28 10:51:34 2010 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Wed Apr 28 11:09:19 2010 +0200
@@ -45,7 +45,7 @@
   thy
   |> Theory.copy
   |> Sign.root_path
-  |> Sign.add_defsort_i []
+  |> Sign.set_defsort []
   |> Sign.add_types [(Binding.name "proof", 0, NoSyn)]
   |> fold (snd oo Sign.declare_const)
       [((Binding.name "Appt", [proofT, aT] ---> proofT), Mixfix ("(1_ %/ _)", [4, 5], 4)),
diff -r edb757388592 -r 78721f3adb13 src/Pure/sign.ML
--- 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) =>