--- a/src/HOL/Import/HOLLight/hollight.imp Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/HOLLight/hollight.imp Thu Jan 28 11:48:49 2010 +0100
@@ -238,10 +238,10 @@
"<=" > "HOLLight.hollight.<="
"<" > "HOLLight.hollight.<"
"/\\" > "op &"
- "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
+ "-" > "Algebras.minus_class.minus" :: "nat => nat => nat"
"," > "Pair"
- "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
- "*" > "HOL.times_class.times" :: "nat => nat => nat"
+ "+" > "Algebras.plus_class.plus" :: "nat => nat => nat"
+ "*" > "Algebras.times_class.times" :: "nat => nat => nat"
"$" > "HOLLight.hollight.$"
"!" > "All"