diff -r 8d710bece29f -r 61bdf2ae4dc5 src/HOL/ex/Higher_Order_Logic.thy
--- a/src/HOL/ex/Higher_Order_Logic.thy	Tue Jun 01 11:25:26 2004 +0200
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Tue Jun 01 12:33:50 2004 +0200
@@ -20,7 +20,7 @@
 
 subsection {* Pure Logic *}
 
-classes type \<subseteq> logic
+classes type
 defaultsort type
 
 typedecl o