modernized/simplified Sign.set_defsort;
authorwenzelm
Wed Apr 28 11:09:19 2010 +0200 (2010-04-28)
changeset 3644978721f3adb13
parent 36448 edb757388592
child 36450 62eaaffe6e47
modernized/simplified Sign.set_defsort;
src/Pure/Isar/isar_syn.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Apr 28 10:51:34 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 28 11:09:19 2010 +0200
     1.3 @@ -97,7 +97,8 @@
     1.4  
     1.5  val _ =
     1.6    OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
     1.7 -    (P.sort >> (Toplevel.theory o Sign.add_defsort));
     1.8 +    (P.sort >>
     1.9 +      (fn s => Toplevel.theory (fn thy => Sign.set_defsort (Syntax.read_sort_global thy s) thy)));
    1.10  
    1.11  
    1.12  (* types *)
     2.1 --- a/src/Pure/Proof/proof_syntax.ML	Wed Apr 28 10:51:34 2010 +0200
     2.2 +++ b/src/Pure/Proof/proof_syntax.ML	Wed Apr 28 11:09:19 2010 +0200
     2.3 @@ -45,7 +45,7 @@
     2.4    thy
     2.5    |> Theory.copy
     2.6    |> Sign.root_path
     2.7 -  |> Sign.add_defsort_i []
     2.8 +  |> Sign.set_defsort []
     2.9    |> Sign.add_types [(Binding.name "proof", 0, NoSyn)]
    2.10    |> fold (snd oo Sign.declare_const)
    2.11        [((Binding.name "Appt", [proofT, aT] ---> proofT), Mixfix ("(1_ %/ _)", [4, 5], 4)),
     3.1 --- a/src/Pure/sign.ML	Wed Apr 28 10:51:34 2010 +0200
     3.2 +++ b/src/Pure/sign.ML	Wed Apr 28 11:09:19 2010 +0200
     3.3 @@ -25,6 +25,7 @@
     3.4    val super_classes: theory -> class -> class list
     3.5    val minimize_sort: theory -> sort -> sort
     3.6    val complete_sort: theory -> sort -> sort
     3.7 +  val set_defsort: sort -> theory -> theory
     3.8    val defaultS: theory -> sort
     3.9    val subsort: theory -> sort * sort -> bool
    3.10    val of_sort: theory -> typ * sort -> bool
    3.11 @@ -68,8 +69,6 @@
    3.12    val cert_prop: theory -> term -> term
    3.13    val no_frees: Pretty.pp -> term -> term
    3.14    val no_vars: Pretty.pp -> term -> term
    3.15 -  val add_defsort: string -> theory -> theory
    3.16 -  val add_defsort_i: sort -> theory -> theory
    3.17    val add_types: (binding * int * mixfix) list -> theory -> theory
    3.18    val add_nonterminals: binding list -> theory -> theory
    3.19    val add_type_abbrev: binding * string list * typ -> theory -> theory
    3.20 @@ -198,6 +197,7 @@
    3.21  val minimize_sort = Sorts.minimize_sort o classes_of;
    3.22  val complete_sort = Sorts.complete_sort o classes_of;
    3.23  
    3.24 +val set_defsort = map_tsig o Type.set_defsort;
    3.25  val defaultS = Type.defaultS o tsig_of;
    3.26  val subsort = Type.subsort o tsig_of;
    3.27  val of_sort = Type.of_sort o tsig_of;
    3.28 @@ -334,15 +334,6 @@
    3.29  
    3.30  (** signature extension functions **)  (*exception ERROR/TYPE*)
    3.31  
    3.32 -(* add default sort *)
    3.33 -
    3.34 -fun gen_add_defsort prep_sort s thy =
    3.35 -  thy |> map_tsig (Type.set_defsort (prep_sort thy s));
    3.36 -
    3.37 -val add_defsort = gen_add_defsort Syntax.read_sort_global;
    3.38 -val add_defsort_i = gen_add_defsort certify_sort;
    3.39 -
    3.40 -
    3.41  (* add type constructors *)
    3.42  
    3.43  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>