--- a/src/HOLCF/Tutorial/New_Domain.thy	Wed Nov 10 09:59:08 2010 -0800
+++ b/src/HOLCF/Tutorial/New_Domain.thy	Wed Nov 10 11:42:35 2010 -0800
@@ -13,10 +13,8 @@
   package. This file should be merged with @{text Domain_ex.thy}.
 *}
 
-default_sort bifinite
-
 text {*
-  Provided that @{text bifinite} is the default sort, the @{text new_domain}
+  Provided that @{text domain} is the default sort, the @{text new_domain}
   package should work with any type definition supported by the old
   domain package.
 *}