diff -r 466e714de2fc -r c03e9d04b3e4 src/HOL/Import/HOL/realax.imp
--- a/src/HOL/Import/HOL/realax.imp	Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Import/HOL/realax.imp	Wed Jan 02 15:14:02 2008 +0100
@@ -27,7 +27,7 @@
   "treal_add" > "HOL4Real.realax.treal_add"
   "treal_1" > "HOL4Real.realax.treal_1"
   "treal_0" > "HOL4Real.realax.treal_0"
-  "real_neg" > "HOL.minus_class.uminus" :: "real => real"
+  "real_neg" > "HOL.uminus_class.uminus" :: "real => real"
   "real_mul" > "HOL.times_class.times" :: "real => real => real"
   "real_lt" > "HOL.ord_class.less" :: "real => real => bool"
   "real_add" > "HOL.plus_class.plus" :: "real => real => real"