--- a/src/HOL/Import/HOLLight/hollight.imp	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Import/HOLLight/hollight.imp	Fri Mar 10 15:33:48 2006 +0100
@@ -238,10 +238,10 @@
   "<=" > "HOLLight.hollight.<="
   "<" > "HOLLight.hollight.<"
   "/\\" > "op &"
-  "-" > "op -" :: "nat => nat => nat"
+  "-" > "HOL.minus" :: "nat => nat => nat"
   "," > "Pair"
-  "+" > "op +" :: "nat => nat => nat"
-  "*" > "op *" :: "nat => nat => nat"
+  "+" > "HOL.plus" :: "nat => nat => nat"
+  "*" > "HOL.times" :: "nat => nat => nat"
   "$" > "HOLLight.hollight.$"
   "!" > "All"