--- a/src/HOL/ex/Higher_Order_Logic.thy Wed Sep 13 00:38:38 2006 +0200
+++ b/src/HOL/ex/Higher_Order_Logic.thy Wed Sep 13 12:05:50 2006 +0200
@@ -25,7 +25,7 @@
typedecl o
arities
o :: type
- fun :: (type, type) type
+ "fun" :: (type, type) type
subsubsection {* Basic logical connectives *}