diff -r 9701dbc35f86 -r 4de48353034e src/HOL/ex/Higher_Order_Logic.thy
--- a/src/HOL/ex/Higher_Order_Logic.thy	Mon Feb 10 14:33:47 2014 +0100
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Mon Feb 10 17:20:11 2014 +0100
@@ -18,13 +18,12 @@
 
 subsection {* Pure Logic *}
 
-classes type
+class type
 default_sort type
 
 typedecl o
-arities
-  o :: type
-  "fun" :: (type, type) type
+instance o :: type ..
+instance "fun" :: (type, type) type ..
 
 
 subsubsection {* Basic logical connectives *}