renamed command 'defaultsort' to 'default_sort';
authorwenzelm
Wed Apr 28 12:07:52 2010 +0200 (2010-04-28)
changeset 36452d37c6eed8117
parent 36451 ddc965e172c4
child 36453 2f383885d8f8
renamed command 'defaultsort' to 'default_sort';
src/CCL/CCL.thy
src/FOL/IFOL.thy
src/FOLP/IFOLP.thy
src/HOL/HOL.thy
src/HOL/ex/Higher_Order_Logic.thy
src/HOLCF/Adm.thy
src/HOLCF/Algebraic.thy
src/HOLCF/Cfun.thy
src/HOLCF/CompactBasis.thy
src/HOLCF/Cont.thy
src/HOLCF/Cprod.thy
src/HOLCF/Deflation.thy
src/HOLCF/Domain.thy
src/HOLCF/FOCUS/Fstream.thy
src/HOLCF/FOCUS/Fstreams.thy
src/HOLCF/Fix.thy
src/HOLCF/Fixrec.thy
src/HOLCF/HOLCF.thy
src/HOLCF/IOA/Storage/Correctness.thy
src/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOLCF/IOA/meta_theory/Automata.thy
src/HOLCF/IOA/meta_theory/LiveIOA.thy
src/HOLCF/IOA/meta_theory/Pred.thy
src/HOLCF/IOA/meta_theory/RefMappings.thy
src/HOLCF/IOA/meta_theory/Sequence.thy
src/HOLCF/IOA/meta_theory/Simulations.thy
src/HOLCF/IOA/meta_theory/TL.thy
src/HOLCF/IOA/meta_theory/TLS.thy
src/HOLCF/IOA/meta_theory/Traces.thy
src/HOLCF/Lift.thy
src/HOLCF/Product_Cpo.thy
src/HOLCF/Representable.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Tr.thy
src/HOLCF/Universal.thy
src/HOLCF/Up.thy
src/HOLCF/ex/Domain_Proofs.thy
src/HOLCF/ex/Letrec.thy
src/HOLCF/ex/New_Domain.thy
src/HOLCF/ex/Powerdomain_ex.thy
src/LCF/LCF.thy
src/Pure/Isar/isar_syn.ML
src/Sequents/LK0.thy
     1.1 --- a/src/CCL/CCL.thy	Wed Apr 28 11:41:27 2010 +0200
     1.2 +++ b/src/CCL/CCL.thy	Wed Apr 28 12:07:52 2010 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  *}
     1.5  
     1.6  classes prog < "term"
     1.7 -defaultsort prog
     1.8 +default_sort prog
     1.9  
    1.10  arities "fun" :: (prog, prog) prog
    1.11  
     2.1 --- a/src/FOL/IFOL.thy	Wed Apr 28 11:41:27 2010 +0200
     2.2 +++ b/src/FOL/IFOL.thy	Wed Apr 28 12:07:52 2010 +0200
     2.3 @@ -31,7 +31,7 @@
     2.4  global
     2.5  
     2.6  classes "term"
     2.7 -defaultsort "term"
     2.8 +default_sort "term"
     2.9  
    2.10  typedecl o
    2.11  
     3.1 --- a/src/FOLP/IFOLP.thy	Wed Apr 28 11:41:27 2010 +0200
     3.2 +++ b/src/FOLP/IFOLP.thy	Wed Apr 28 12:07:52 2010 +0200
     3.3 @@ -15,7 +15,7 @@
     3.4  global
     3.5  
     3.6  classes "term"
     3.7 -defaultsort "term"
     3.8 +default_sort "term"
     3.9  
    3.10  typedecl p
    3.11  typedecl o
     4.1 --- a/src/HOL/HOL.thy	Wed Apr 28 11:41:27 2010 +0200
     4.2 +++ b/src/HOL/HOL.thy	Wed Apr 28 12:07:52 2010 +0200
     4.3 @@ -40,7 +40,7 @@
     4.4  subsubsection {* Core syntax *}
     4.5  
     4.6  classes type
     4.7 -defaultsort type
     4.8 +default_sort type
     4.9  setup {* Object_Logic.add_base_sort @{sort type} *}
    4.10  
    4.11  arities
     5.1 --- a/src/HOL/ex/Higher_Order_Logic.thy	Wed Apr 28 11:41:27 2010 +0200
     5.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy	Wed Apr 28 12:07:52 2010 +0200
     5.3 @@ -20,7 +20,7 @@
     5.4  subsection {* Pure Logic *}
     5.5  
     5.6  classes type
     5.7 -defaultsort type
     5.8 +default_sort type
     5.9  
    5.10  typedecl o
    5.11  arities
     6.1 --- a/src/HOLCF/Adm.thy	Wed Apr 28 11:41:27 2010 +0200
     6.2 +++ b/src/HOLCF/Adm.thy	Wed Apr 28 12:07:52 2010 +0200
     6.3 @@ -8,7 +8,7 @@
     6.4  imports Cont
     6.5  begin
     6.6  
     6.7 -defaultsort cpo
     6.8 +default_sort cpo
     6.9  
    6.10  subsection {* Definitions *}
    6.11  
     7.1 --- a/src/HOLCF/Algebraic.thy	Wed Apr 28 11:41:27 2010 +0200
     7.2 +++ b/src/HOLCF/Algebraic.thy	Wed Apr 28 12:07:52 2010 +0200
     7.3 @@ -297,7 +297,7 @@
     7.4  
     7.5  subsection {* Type constructor for finite deflations *}
     7.6  
     7.7 -defaultsort profinite
     7.8 +default_sort profinite
     7.9  
    7.10  typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
    7.11  by (fast intro: finite_deflation_approx)
     8.1 --- a/src/HOLCF/Cfun.thy	Wed Apr 28 11:41:27 2010 +0200
     8.2 +++ b/src/HOLCF/Cfun.thy	Wed Apr 28 12:07:52 2010 +0200
     8.3 @@ -9,7 +9,7 @@
     8.4  imports Pcpodef Ffun Product_Cpo
     8.5  begin
     8.6  
     8.7 -defaultsort cpo
     8.8 +default_sort cpo
     8.9  
    8.10  subsection {* Definition of continuous function type *}
    8.11  
    8.12 @@ -511,7 +511,7 @@
    8.13  
    8.14  subsection {* Strictified functions *}
    8.15  
    8.16 -defaultsort pcpo
    8.17 +default_sort pcpo
    8.18  
    8.19  definition
    8.20    strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
     9.1 --- a/src/HOLCF/CompactBasis.thy	Wed Apr 28 11:41:27 2010 +0200
     9.2 +++ b/src/HOLCF/CompactBasis.thy	Wed Apr 28 12:07:52 2010 +0200
     9.3 @@ -10,7 +10,7 @@
     9.4  
     9.5  subsection {* Compact bases of bifinite domains *}
     9.6  
     9.7 -defaultsort profinite
     9.8 +default_sort profinite
     9.9  
    9.10  typedef (open) 'a compact_basis = "{x::'a::profinite. compact x}"
    9.11  by (fast intro: compact_approx)
    10.1 --- a/src/HOLCF/Cont.thy	Wed Apr 28 11:41:27 2010 +0200
    10.2 +++ b/src/HOLCF/Cont.thy	Wed Apr 28 12:07:52 2010 +0200
    10.3 @@ -14,7 +14,7 @@
    10.4     of default class po
    10.5  *}
    10.6  
    10.7 -defaultsort po
    10.8 +default_sort po
    10.9  
   10.10  subsection {* Definitions *}
   10.11  
    11.1 --- a/src/HOLCF/Cprod.thy	Wed Apr 28 11:41:27 2010 +0200
    11.2 +++ b/src/HOLCF/Cprod.thy	Wed Apr 28 12:07:52 2010 +0200
    11.3 @@ -8,7 +8,7 @@
    11.4  imports Bifinite
    11.5  begin
    11.6  
    11.7 -defaultsort cpo
    11.8 +default_sort cpo
    11.9  
   11.10  subsection {* Continuous case function for unit type *}
   11.11  
    12.1 --- a/src/HOLCF/Deflation.thy	Wed Apr 28 11:41:27 2010 +0200
    12.2 +++ b/src/HOLCF/Deflation.thy	Wed Apr 28 12:07:52 2010 +0200
    12.3 @@ -8,7 +8,7 @@
    12.4  imports Cfun
    12.5  begin
    12.6  
    12.7 -defaultsort cpo
    12.8 +default_sort cpo
    12.9  
   12.10  subsection {* Continuous deflations *}
   12.11  
    13.1 --- a/src/HOLCF/Domain.thy	Wed Apr 28 11:41:27 2010 +0200
    13.2 +++ b/src/HOLCF/Domain.thy	Wed Apr 28 12:07:52 2010 +0200
    13.3 @@ -16,7 +16,7 @@
    13.4    ("Tools/Domain/domain_extender.ML")
    13.5  begin
    13.6  
    13.7 -defaultsort pcpo
    13.8 +default_sort pcpo
    13.9  
   13.10  
   13.11  subsection {* Casedist *}
    14.1 --- a/src/HOLCF/FOCUS/Fstream.thy	Wed Apr 28 11:41:27 2010 +0200
    14.2 +++ b/src/HOLCF/FOCUS/Fstream.thy	Wed Apr 28 12:07:52 2010 +0200
    14.3 @@ -12,7 +12,7 @@
    14.4  imports "../ex/Stream"
    14.5  begin
    14.6  
    14.7 -defaultsort type
    14.8 +default_sort type
    14.9  
   14.10  types 'a fstream = "'a lift stream"
   14.11  
    15.1 --- a/src/HOLCF/FOCUS/Fstreams.thy	Wed Apr 28 11:41:27 2010 +0200
    15.2 +++ b/src/HOLCF/FOCUS/Fstreams.thy	Wed Apr 28 12:07:52 2010 +0200
    15.3 @@ -8,7 +8,7 @@
    15.4  
    15.5  theory Fstreams imports "../ex/Stream" begin
    15.6  
    15.7 -defaultsort type
    15.8 +default_sort type
    15.9  
   15.10  types 'a fstream = "('a lift) stream"
   15.11  
    16.1 --- a/src/HOLCF/Fix.thy	Wed Apr 28 11:41:27 2010 +0200
    16.2 +++ b/src/HOLCF/Fix.thy	Wed Apr 28 12:07:52 2010 +0200
    16.3 @@ -9,7 +9,7 @@
    16.4  imports Cfun
    16.5  begin
    16.6  
    16.7 -defaultsort pcpo
    16.8 +default_sort pcpo
    16.9  
   16.10  subsection {* Iteration *}
   16.11  
    17.1 --- a/src/HOLCF/Fixrec.thy	Wed Apr 28 11:41:27 2010 +0200
    17.2 +++ b/src/HOLCF/Fixrec.thy	Wed Apr 28 12:07:52 2010 +0200
    17.3 @@ -13,7 +13,7 @@
    17.4  
    17.5  subsection {* Maybe monad type *}
    17.6  
    17.7 -defaultsort cpo
    17.8 +default_sort cpo
    17.9  
   17.10  pcpodef (open) 'a maybe = "UNIV::(one ++ 'a u) set"
   17.11  by simp_all
   17.12 @@ -463,7 +463,7 @@
   17.13  
   17.14  subsection {* Match functions for built-in types *}
   17.15  
   17.16 -defaultsort pcpo
   17.17 +default_sort pcpo
   17.18  
   17.19  definition
   17.20    match_UU :: "'a \<rightarrow> 'c maybe \<rightarrow> 'c maybe"
    18.1 --- a/src/HOLCF/HOLCF.thy	Wed Apr 28 11:41:27 2010 +0200
    18.2 +++ b/src/HOLCF/HOLCF.thy	Wed Apr 28 12:07:52 2010 +0200
    18.3 @@ -12,7 +12,7 @@
    18.4    Sum_Cpo
    18.5  begin
    18.6  
    18.7 -defaultsort pcpo
    18.8 +default_sort pcpo
    18.9  
   18.10  text {* Legacy theorem names *}
   18.11  
    19.1 --- a/src/HOLCF/IOA/Storage/Correctness.thy	Wed Apr 28 11:41:27 2010 +0200
    19.2 +++ b/src/HOLCF/IOA/Storage/Correctness.thy	Wed Apr 28 12:07:52 2010 +0200
    19.3 @@ -8,7 +8,7 @@
    19.4  imports SimCorrectness Spec Impl
    19.5  begin
    19.6  
    19.7 -defaultsort type
    19.8 +default_sort type
    19.9  
   19.10  definition
   19.11    sim_relation :: "((nat * bool) * (nat set * bool)) set" where
    20.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Wed Apr 28 11:41:27 2010 +0200
    20.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Wed Apr 28 12:07:52 2010 +0200
    20.3 @@ -9,7 +9,7 @@
    20.4  uses ("automaton.ML")
    20.5  begin
    20.6  
    20.7 -defaultsort type
    20.8 +default_sort type
    20.9  
   20.10  definition
   20.11    cex_abs :: "('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution" where
    21.1 --- a/src/HOLCF/IOA/meta_theory/Automata.thy	Wed Apr 28 11:41:27 2010 +0200
    21.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Wed Apr 28 12:07:52 2010 +0200
    21.3 @@ -8,7 +8,7 @@
    21.4  imports Asig
    21.5  begin
    21.6  
    21.7 -defaultsort type
    21.8 +default_sort type
    21.9  
   21.10  types
   21.11    ('a, 's) transition = "'s * 'a * 's"
    22.1 --- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Wed Apr 28 11:41:27 2010 +0200
    22.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Wed Apr 28 12:07:52 2010 +0200
    22.3 @@ -8,7 +8,7 @@
    22.4  imports TLS
    22.5  begin
    22.6  
    22.7 -defaultsort type
    22.8 +default_sort type
    22.9  
   22.10  types
   22.11    ('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp"
    23.1 --- a/src/HOLCF/IOA/meta_theory/Pred.thy	Wed Apr 28 11:41:27 2010 +0200
    23.2 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Wed Apr 28 12:07:52 2010 +0200
    23.3 @@ -8,7 +8,7 @@
    23.4  imports Main
    23.5  begin
    23.6  
    23.7 -defaultsort type
    23.8 +default_sort type
    23.9  
   23.10  types
   23.11    'a predicate = "'a => bool"
    24.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.thy	Wed Apr 28 11:41:27 2010 +0200
    24.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy	Wed Apr 28 12:07:52 2010 +0200
    24.3 @@ -8,7 +8,7 @@
    24.4  imports Traces
    24.5  begin
    24.6  
    24.7 -defaultsort type
    24.8 +default_sort type
    24.9  
   24.10  definition
   24.11    move :: "[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" where
    25.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed Apr 28 11:41:27 2010 +0200
    25.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed Apr 28 12:07:52 2010 +0200
    25.3 @@ -8,7 +8,7 @@
    25.4  imports Seq
    25.5  begin
    25.6  
    25.7 -defaultsort type
    25.8 +default_sort type
    25.9  
   25.10  types 'a Seq = "'a::type lift seq"
   25.11  
    26.1 --- a/src/HOLCF/IOA/meta_theory/Simulations.thy	Wed Apr 28 11:41:27 2010 +0200
    26.2 +++ b/src/HOLCF/IOA/meta_theory/Simulations.thy	Wed Apr 28 12:07:52 2010 +0200
    26.3 @@ -8,7 +8,7 @@
    26.4  imports RefCorrectness
    26.5  begin
    26.6  
    26.7 -defaultsort type
    26.8 +default_sort type
    26.9  
   26.10  definition
   26.11    is_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
    27.1 --- a/src/HOLCF/IOA/meta_theory/TL.thy	Wed Apr 28 11:41:27 2010 +0200
    27.2 +++ b/src/HOLCF/IOA/meta_theory/TL.thy	Wed Apr 28 12:07:52 2010 +0200
    27.3 @@ -8,7 +8,7 @@
    27.4  imports Pred Sequence
    27.5  begin
    27.6  
    27.7 -defaultsort type
    27.8 +default_sort type
    27.9  
   27.10  types
   27.11    'a temporal = "'a Seq predicate"
    28.1 --- a/src/HOLCF/IOA/meta_theory/TLS.thy	Wed Apr 28 11:41:27 2010 +0200
    28.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Wed Apr 28 12:07:52 2010 +0200
    28.3 @@ -8,7 +8,7 @@
    28.4  imports IOA TL
    28.5  begin
    28.6  
    28.7 -defaultsort type
    28.8 +default_sort type
    28.9  
   28.10  types
   28.11    ('a, 's) ioa_temp  = "('a option,'s)transition temporal"
    29.1 --- a/src/HOLCF/IOA/meta_theory/Traces.thy	Wed Apr 28 11:41:27 2010 +0200
    29.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Wed Apr 28 12:07:52 2010 +0200
    29.3 @@ -8,7 +8,7 @@
    29.4  imports Sequence Automata
    29.5  begin
    29.6  
    29.7 -defaultsort type
    29.8 +default_sort type
    29.9  
   29.10  types
   29.11     ('a,'s)pairs            =    "('a * 's) Seq"
    30.1 --- a/src/HOLCF/Lift.thy	Wed Apr 28 11:41:27 2010 +0200
    30.2 +++ b/src/HOLCF/Lift.thy	Wed Apr 28 12:07:52 2010 +0200
    30.3 @@ -8,7 +8,7 @@
    30.4  imports Discrete Up Countable
    30.5  begin
    30.6  
    30.7 -defaultsort type
    30.8 +default_sort type
    30.9  
   30.10  pcpodef 'a lift = "UNIV :: 'a discr u set"
   30.11  by simp_all
    31.1 --- a/src/HOLCF/Product_Cpo.thy	Wed Apr 28 11:41:27 2010 +0200
    31.2 +++ b/src/HOLCF/Product_Cpo.thy	Wed Apr 28 12:07:52 2010 +0200
    31.3 @@ -8,7 +8,7 @@
    31.4  imports Adm
    31.5  begin
    31.6  
    31.7 -defaultsort cpo
    31.8 +default_sort cpo
    31.9  
   31.10  subsection {* Unit type is a pcpo *}
   31.11  
    32.1 --- a/src/HOLCF/Representable.thy	Wed Apr 28 11:41:27 2010 +0200
    32.2 +++ b/src/HOLCF/Representable.thy	Wed Apr 28 12:07:52 2010 +0200
    32.3 @@ -42,7 +42,7 @@
    32.4    @{term rep}, unless specified otherwise.
    32.5  *}
    32.6  
    32.7 -defaultsort rep
    32.8 +default_sort rep
    32.9  
   32.10  subsection {* Representations of types *}
   32.11  
    33.1 --- a/src/HOLCF/Sprod.thy	Wed Apr 28 11:41:27 2010 +0200
    33.2 +++ b/src/HOLCF/Sprod.thy	Wed Apr 28 12:07:52 2010 +0200
    33.3 @@ -8,7 +8,7 @@
    33.4  imports Bifinite
    33.5  begin
    33.6  
    33.7 -defaultsort pcpo
    33.8 +default_sort pcpo
    33.9  
   33.10  subsection {* Definition of strict product type *}
   33.11  
    34.1 --- a/src/HOLCF/Ssum.thy	Wed Apr 28 11:41:27 2010 +0200
    34.2 +++ b/src/HOLCF/Ssum.thy	Wed Apr 28 12:07:52 2010 +0200
    34.3 @@ -8,7 +8,7 @@
    34.4  imports Tr
    34.5  begin
    34.6  
    34.7 -defaultsort pcpo
    34.8 +default_sort pcpo
    34.9  
   34.10  subsection {* Definition of strict sum type *}
   34.11  
    35.1 --- a/src/HOLCF/Tr.thy	Wed Apr 28 11:41:27 2010 +0200
    35.2 +++ b/src/HOLCF/Tr.thy	Wed Apr 28 12:07:52 2010 +0200
    35.3 @@ -62,7 +62,7 @@
    35.4  
    35.5  subsection {* Case analysis *}
    35.6  
    35.7 -defaultsort pcpo
    35.8 +default_sort pcpo
    35.9  
   35.10  definition
   35.11    trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where
    36.1 --- a/src/HOLCF/Universal.thy	Wed Apr 28 11:41:27 2010 +0200
    36.2 +++ b/src/HOLCF/Universal.thy	Wed Apr 28 12:07:52 2010 +0200
    36.3 @@ -340,7 +340,7 @@
    36.4  
    36.5  subsection {* Universality of \emph{udom} *}
    36.6  
    36.7 -defaultsort bifinite
    36.8 +default_sort bifinite
    36.9  
   36.10  subsubsection {* Choosing a maximal element from a finite set *}
   36.11  
    37.1 --- a/src/HOLCF/Up.thy	Wed Apr 28 11:41:27 2010 +0200
    37.2 +++ b/src/HOLCF/Up.thy	Wed Apr 28 12:07:52 2010 +0200
    37.3 @@ -8,7 +8,7 @@
    37.4  imports Bifinite
    37.5  begin
    37.6  
    37.7 -defaultsort cpo
    37.8 +default_sort cpo
    37.9  
   37.10  subsection {* Definition of new type for lifting *}
   37.11  
    38.1 --- a/src/HOLCF/ex/Domain_Proofs.thy	Wed Apr 28 11:41:27 2010 +0200
    38.2 +++ b/src/HOLCF/ex/Domain_Proofs.thy	Wed Apr 28 12:07:52 2010 +0200
    38.3 @@ -8,7 +8,7 @@
    38.4  imports HOLCF
    38.5  begin
    38.6  
    38.7 -defaultsort rep
    38.8 +default_sort rep
    38.9  
   38.10  (*
   38.11  
    39.1 --- a/src/HOLCF/ex/Letrec.thy	Wed Apr 28 11:41:27 2010 +0200
    39.2 +++ b/src/HOLCF/ex/Letrec.thy	Wed Apr 28 12:07:52 2010 +0200
    39.3 @@ -8,7 +8,7 @@
    39.4  imports HOLCF
    39.5  begin
    39.6  
    39.7 -defaultsort pcpo
    39.8 +default_sort pcpo
    39.9  
   39.10  definition
   39.11    CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
    40.1 --- a/src/HOLCF/ex/New_Domain.thy	Wed Apr 28 11:41:27 2010 +0200
    40.2 +++ b/src/HOLCF/ex/New_Domain.thy	Wed Apr 28 12:07:52 2010 +0200
    40.3 @@ -13,7 +13,7 @@
    40.4    i.e. types in class @{text rep}.
    40.5  *}
    40.6  
    40.7 -defaultsort rep
    40.8 +default_sort rep
    40.9  
   40.10  text {*
   40.11    Provided that @{text rep} is the default sort, the @{text new_domain}
    41.1 --- a/src/HOLCF/ex/Powerdomain_ex.thy	Wed Apr 28 11:41:27 2010 +0200
    41.2 +++ b/src/HOLCF/ex/Powerdomain_ex.thy	Wed Apr 28 12:07:52 2010 +0200
    41.3 @@ -8,7 +8,7 @@
    41.4  imports HOLCF
    41.5  begin
    41.6  
    41.7 -defaultsort bifinite
    41.8 +default_sort bifinite
    41.9  
   41.10  subsection {* Monadic sorting example *}
   41.11  
    42.1 --- a/src/LCF/LCF.thy	Wed Apr 28 11:41:27 2010 +0200
    42.2 +++ b/src/LCF/LCF.thy	Wed Apr 28 12:07:52 2010 +0200
    42.3 @@ -14,7 +14,7 @@
    42.4  subsection {* Natural Deduction Rules for LCF *}
    42.5  
    42.6  classes cpo < "term"
    42.7 -defaultsort cpo
    42.8 +default_sort cpo
    42.9  
   42.10  typedecl tr
   42.11  typedecl void
    43.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Apr 28 11:41:27 2010 +0200
    43.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 28 12:07:52 2010 +0200
    43.3 @@ -96,7 +96,7 @@
    43.4      >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
    43.5  
    43.6  val _ =
    43.7 -  OuterSyntax.local_theory "defaultsort" "declare default sort for explicit type variables"
    43.8 +  OuterSyntax.local_theory "default_sort" "declare default sort for explicit type variables"
    43.9      K.thy_decl
   43.10      (P.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
   43.11  
    44.1 --- a/src/Sequents/LK0.thy	Wed Apr 28 11:41:27 2010 +0200
    44.2 +++ b/src/Sequents/LK0.thy	Wed Apr 28 12:07:52 2010 +0200
    44.3 @@ -15,7 +15,7 @@
    44.4  global
    44.5  
    44.6  classes "term"
    44.7 -defaultsort "term"
    44.8 +default_sort "term"
    44.9  
   44.10  consts
   44.11