src/HOL/HOL.thy

 
 subsection {* Primitive logic *}
 
 subsubsection {* Core syntax *}
 
+classes type < logic
+defaultsort type
+
 global
 
-classes "term" < logic
-defaultsort "term"
-
 typedecl bool
 
 arities
-  bool :: "term"
-  fun :: ("term", "term") "term"
+  bool :: type
+  fun :: (type, type) type
 
 judgment
   Trueprop      :: "bool => prop"                   ("(_)" 5)
 
 consts

     definition syntactically *}
 
 
 subsubsection {* Generic algebraic operations *}
 
-axclass zero < "term"
-axclass one < "term"
-axclass plus < "term"
-axclass minus < "term"
-axclass times < "term"
-axclass inverse < "term"
+axclass zero < type
+axclass one < type
+axclass plus < type
+axclass minus < type
+axclass times < type
+axclass inverse < type
 
 global
 
 consts
   "0"           :: "'a::zero"                       ("0")

 
 
 subsection {* Order signatures and orders *}
 
 axclass
-  ord < "term"
+  ord < type
 
 syntax
   "op <"        :: "['a::ord, 'a] => bool"             ("op <")
   "op <="       :: "['a::ord, 'a] => bool"             ("op <=")