# HG changeset patch
# User wenzelm
# Date 1272449272 -7200
# Node ID d37c6eed81171e83a30c57f7ed6c18cc7943afda
# Parent  ddc965e172c4d4dc46488616249c9622d206de48
renamed command 'defaultsort' to 'default_sort';

diff -r ddc965e172c4 -r d37c6eed8117 src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/CCL/CCL.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -17,7 +17,7 @@
 *}
 
 classes prog < "term"
-defaultsort prog
+default_sort prog
 
 arities "fun" :: (prog, prog) prog
 
diff -r ddc965e172c4 -r d37c6eed8117 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/FOL/IFOL.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -31,7 +31,7 @@
 global
 
 classes "term"
-defaultsort "term"
+default_sort "term"
 
 typedecl o
 
diff -r ddc965e172c4 -r d37c6eed8117 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/FOLP/IFOLP.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -15,7 +15,7 @@
 global
 
 classes "term"
-defaultsort "term"
+default_sort "term"
 
 typedecl p
 typedecl o
diff -r ddc965e172c4 -r d37c6eed8117 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOL/HOL.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -40,7 +40,7 @@
 subsubsection {* Core syntax *}
 
 classes type
-defaultsort type
+default_sort type
 setup {* Object_Logic.add_base_sort @{sort type} *}
 
 arities
diff -r ddc965e172c4 -r d37c6eed8117 src/HOL/ex/Higher_Order_Logic.thy
--- a/src/HOL/ex/Higher_Order_Logic.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -20,7 +20,7 @@
 subsection {* Pure Logic *}
 
 classes type
-defaultsort type
+default_sort type
 
 typedecl o
 arities
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Adm.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports Cont
 begin
 
-defaultsort cpo
+default_sort cpo
 
 subsection {* Definitions *}
 
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Algebraic.thy
--- a/src/HOLCF/Algebraic.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Algebraic.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -297,7 +297,7 @@
 
 subsection {* Type constructor for finite deflations *}
 
-defaultsort profinite
+default_sort profinite
 
 typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
 by (fast intro: finite_deflation_approx)
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Cfun.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -9,7 +9,7 @@
 imports Pcpodef Ffun Product_Cpo
 begin
 
-defaultsort cpo
+default_sort cpo
 
 subsection {* Definition of continuous function type *}
 
@@ -511,7 +511,7 @@
 
 subsection {* Strictified functions *}
 
-defaultsort pcpo
+default_sort pcpo
 
 definition
   strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/CompactBasis.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -10,7 +10,7 @@
 
 subsection {* Compact bases of bifinite domains *}
 
-defaultsort profinite
+default_sort profinite
 
 typedef (open) 'a compact_basis = "{x::'a::profinite. compact x}"
 by (fast intro: compact_approx)
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Cont.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -14,7 +14,7 @@
    of default class po
 *}
 
-defaultsort po
+default_sort po
 
 subsection {* Definitions *}
 
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Cprod.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports Bifinite
 begin
 
-defaultsort cpo
+default_sort cpo
 
 subsection {* Continuous case function for unit type *}
 
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Deflation.thy
--- a/src/HOLCF/Deflation.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Deflation.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports Cfun
 begin
 
-defaultsort cpo
+default_sort cpo
 
 subsection {* Continuous deflations *}
 
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Domain.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -16,7 +16,7 @@
   ("Tools/Domain/domain_extender.ML")
 begin
 
-defaultsort pcpo
+default_sort pcpo
 
 
 subsection {* Casedist *}
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/FOCUS/Fstream.thy
--- a/src/HOLCF/FOCUS/Fstream.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -12,7 +12,7 @@
 imports "../ex/Stream"
 begin
 
-defaultsort type
+default_sort type
 
 types 'a fstream = "'a lift stream"
 
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOLCF/FOCUS/Fstreams.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/FOCUS/Fstreams.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 
 theory Fstreams imports "../ex/Stream" begin
 
-defaultsort type
+default_sort type
 
 types 'a fstream = "('a lift) stream"
 
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Fix.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -9,7 +9,7 @@
 imports Cfun
 begin
 
-defaultsort pcpo
+default_sort pcpo
 
 subsection {* Iteration *}
 
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Fixrec.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -13,7 +13,7 @@
 
 subsection {* Maybe monad type *}
 
-defaultsort cpo
+default_sort cpo
 
 pcpodef (open) 'a maybe = "UNIV::(one ++ 'a u) set"
 by simp_all
@@ -463,7 +463,7 @@
 
 subsection {* Match functions for built-in types *}
 
-defaultsort pcpo
+default_sort pcpo
 
 definition
   match_UU :: "'a \<rightarrow> 'c maybe \<rightarrow> 'c maybe"
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/HOLCF.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -12,7 +12,7 @@
   Sum_Cpo
 begin
 
-defaultsort pcpo
+default_sort pcpo
 
 text {* Legacy theorem names *}
 
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/IOA/Storage/Correctness.thy
--- a/src/HOLCF/IOA/Storage/Correctness.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/IOA/Storage/Correctness.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports SimCorrectness Spec Impl
 begin
 
-defaultsort type
+default_sort type
 
 definition
   sim_relation :: "((nat * bool) * (nat set * bool)) set" where
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -9,7 +9,7 @@
 uses ("automaton.ML")
 begin
 
-defaultsort type
+default_sort type
 
 definition
   cex_abs :: "('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution" where
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOLCF/IOA/meta_theory/Automata.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports Asig
 begin
 
-defaultsort type
+default_sort type
 
 types
   ('a, 's) transition = "'s * 'a * 's"
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/IOA/meta_theory/LiveIOA.thy
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports TLS
 begin
 
-defaultsort type
+default_sort type
 
 types
   ('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp"
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/IOA/meta_theory/Pred.thy
--- a/src/HOLCF/IOA/meta_theory/Pred.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports Main
 begin
 
-defaultsort type
+default_sort type
 
 types
   'a predicate = "'a => bool"
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/IOA/meta_theory/RefMappings.thy
--- a/src/HOLCF/IOA/meta_theory/RefMappings.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports Traces
 begin
 
-defaultsort type
+default_sort type
 
 definition
   move :: "[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" where
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports Seq
 begin
 
-defaultsort type
+default_sort type
 
 types 'a Seq = "'a::type lift seq"
 
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/IOA/meta_theory/Simulations.thy
--- a/src/HOLCF/IOA/meta_theory/Simulations.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/Simulations.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports RefCorrectness
 begin
 
-defaultsort type
+default_sort type
 
 definition
   is_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/IOA/meta_theory/TL.thy
--- a/src/HOLCF/IOA/meta_theory/TL.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/TL.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports Pred Sequence
 begin
 
-defaultsort type
+default_sort type
 
 types
   'a temporal = "'a Seq predicate"
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOLCF/IOA/meta_theory/TLS.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports IOA TL
 begin
 
-defaultsort type
+default_sort type
 
 types
   ('a, 's) ioa_temp  = "('a option,'s)transition temporal"
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOLCF/IOA/meta_theory/Traces.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports Sequence Automata
 begin
 
-defaultsort type
+default_sort type
 
 types
    ('a,'s)pairs            =    "('a * 's) Seq"
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Lift.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports Discrete Up Countable
 begin
 
-defaultsort type
+default_sort type
 
 pcpodef 'a lift = "UNIV :: 'a discr u set"
 by simp_all
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Product_Cpo.thy
--- a/src/HOLCF/Product_Cpo.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Product_Cpo.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports Adm
 begin
 
-defaultsort cpo
+default_sort cpo
 
 subsection {* Unit type is a pcpo *}
 
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Representable.thy
--- a/src/HOLCF/Representable.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Representable.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -42,7 +42,7 @@
   @{term rep}, unless specified otherwise.
 *}
 
-defaultsort rep
+default_sort rep
 
 subsection {* Representations of types *}
 
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Sprod.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports Bifinite
 begin
 
-defaultsort pcpo
+default_sort pcpo
 
 subsection {* Definition of strict product type *}
 
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Ssum.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports Tr
 begin
 
-defaultsort pcpo
+default_sort pcpo
 
 subsection {* Definition of strict sum type *}
 
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Tr.thy
--- a/src/HOLCF/Tr.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Tr.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -62,7 +62,7 @@
 
 subsection {* Case analysis *}
 
-defaultsort pcpo
+default_sort pcpo
 
 definition
   trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Universal.thy
--- a/src/HOLCF/Universal.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Universal.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -340,7 +340,7 @@
 
 subsection {* Universality of \emph{udom} *}
 
-defaultsort bifinite
+default_sort bifinite
 
 subsubsection {* Choosing a maximal element from a finite set *}
 
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/Up.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports Bifinite
 begin
 
-defaultsort cpo
+default_sort cpo
 
 subsection {* Definition of new type for lifting *}
 
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOLCF/ex/Domain_Proofs.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports HOLCF
 begin
 
-defaultsort rep
+default_sort rep
 
 (*
 
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/ex/Letrec.thy
--- a/src/HOLCF/ex/Letrec.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/ex/Letrec.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports HOLCF
 begin
 
-defaultsort pcpo
+default_sort pcpo
 
 definition
   CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/ex/New_Domain.thy
--- a/src/HOLCF/ex/New_Domain.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/ex/New_Domain.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -13,7 +13,7 @@
   i.e. types in class @{text rep}.
 *}
 
-defaultsort rep
+default_sort rep
 
 text {*
   Provided that @{text rep} is the default sort, the @{text new_domain}
diff -r ddc965e172c4 -r d37c6eed8117 src/HOLCF/ex/Powerdomain_ex.thy
--- a/src/HOLCF/ex/Powerdomain_ex.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/HOLCF/ex/Powerdomain_ex.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -8,7 +8,7 @@
 imports HOLCF
 begin
 
-defaultsort bifinite
+default_sort bifinite
 
 subsection {* Monadic sorting example *}
 
diff -r ddc965e172c4 -r d37c6eed8117 src/LCF/LCF.thy
--- a/src/LCF/LCF.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/LCF/LCF.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -14,7 +14,7 @@
 subsection {* Natural Deduction Rules for LCF *}
 
 classes cpo < "term"
-defaultsort cpo
+default_sort cpo
 
 typedecl tr
 typedecl void
diff -r ddc965e172c4 -r d37c6eed8117 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 28 12:07:52 2010 +0200
@@ -96,7 +96,7 @@
     >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
 
 val _ =
-  OuterSyntax.local_theory "defaultsort" "declare default sort for explicit type variables"
+  OuterSyntax.local_theory "default_sort" "declare default sort for explicit type variables"
     K.thy_decl
     (P.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
 
diff -r ddc965e172c4 -r d37c6eed8117 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Wed Apr 28 11:41:27 2010 +0200
+++ b/src/Sequents/LK0.thy	Wed Apr 28 12:07:52 2010 +0200
@@ -15,7 +15,7 @@
 global
 
 classes "term"
-defaultsort "term"
+default_sort "term"
 
 consts