diff -r 5d53e3f35152 -r 416b2ecd97a1 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Jul 16 20:47:45 2000 +0200
+++ b/src/HOL/HOL.thy	Sun Jul 16 20:48:35 2000 +0200
@@ -113,7 +113,6 @@
   "op &"        :: "[bool, bool] => bool"                (infixr "\\<and>" 35)
   "op |"        :: "[bool, bool] => bool"                (infixr "\\<or>" 30)
   "op -->"      :: "[bool, bool] => bool"                (infixr "\\<midarrow>\\<rightarrow>" 25)
-  "op o"        :: "['b => 'c, 'a => 'b, 'a] => 'c"      (infixl "\\<circ>" 55)
   "op ~="       :: "['a, 'a] => bool"                    (infixl "\\<noteq>" 50)
   "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\\<epsilon>_./ _)" [0, 10] 10)
   "ALL "        :: "[idts, bool] => bool"                ("(3\\<forall>_./ _)" [0, 10] 10)