src/HOLCF/Fixrec.thy
changeset 36452 d37c6eed8117
parent 36176 3fe7e97ccca8
child 36998 9316a18ec931
--- 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"