--- 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"