src/HOL/Import/Generate-HOLLight/GenHOLLight.thy

--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Jun 10 12:24:03 2010 +0200
@@ -38,9 +38,9 @@
   bool > bool
   fun > fun
   N_1 >  Product_Type.unit
-  prod > "*"
-  num > nat
-  sum > "+"
+  prod > "Product_Type.*"
+  num > Nat.nat
+  sum > "Sum_Type.+"
 (*  option > Datatype.option*);
 
 const_renames