--- a/src/HOL/HOL.thy Mon Feb 10 22:07:50 2014 +0100
+++ b/src/HOL/HOL.thy Mon Feb 10 22:08:18 2014 +0100
@@ -45,7 +45,7 @@
subsubsection {* Core syntax *}
-classes type
+setup {* Axclass.axiomatize_class (@{binding type}, []) *}
default_sort type
setup {* Object_Logic.add_base_sort @{sort type} *}