diff -r ac7ea72c463b -r 916b9df2ce9f src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sat Apr 23 19:49:08 2005 +0200
+++ b/src/HOL/Orderings.thy	Sat Apr 23 19:49:16 2005 +0200
@@ -39,7 +39,7 @@
 
 text{* Syntactic sugar: *}
 
-consts
+syntax
   "_gt" :: "'a::ord => 'a => bool"             (infixl ">" 50)
   "_ge" :: "'a::ord => 'a => bool"             (infixl ">=" 50)
 translations