src/HOL/HOL.thy
changeset 36452 d37c6eed8117
parent 36365 18bf20d0c2df
child 36532 fdfc37254090
--- 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