src/HOL/Main.thy

--- a/src/HOL/Main.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Main.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -60,8 +60,8 @@
   top ("\<top>") and
   inf (infixl "\<sqinter>" 70) and
   sup (infixl "\<squnion>" 65) and
-  Inf ("\<Sqinter> _" [900] 900) and
-  Sup ("\<Squnion> _" [900] 900) and
+  Inf ("\<Sqinter>") and
+  Sup ("\<Squnion>") and
   ordLeq2 (infix "<=o" 50) and
   ordLeq3 (infix "\<le>o" 50) and
   ordLess2 (infix "<o" 50) and