diff -r c5a8b612e571 -r 0040bafffdef src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Jul 01 16:54:44 2010 +0200
@@ -38,9 +38,9 @@
   bool > bool
   fun > fun
   N_1 >  Product_Type.unit
-  prod > "Product_Type.*"
+  prod > Product_Type.prod
   num > Nat.nat
-  sum > "Sum_Type.+"
+  sum > Sum_Type.sum
 (*  option > Datatype.option*);
 
 const_renames