diff -r e58bb0f57c0c -r 9a2c90bdadfe src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Oct 31 12:46:21 1998 +0100
+++ b/src/HOL/HOL.thy	Mon Nov 02 12:35:14 1998 +0100
@@ -70,7 +70,7 @@
 consts
   "+"           :: ['a::plus, 'a]  => 'a            (infixl 65)
   "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
-  uminus        :: ['a::minus] => 'a                ("- _" [80] 80)
+  uminus        :: ['a::minus] => 'a                ("- _" [100] 100)
   "*"           :: ['a::times, 'a] => 'a            (infixl 70)
   (*See Nat.thy for "^"*)