diff -r 2e9bf718a7a1 -r 65631ca437c9 src/LCF/LCF.thy
--- a/src/LCF/LCF.thy	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/LCF/LCF.thy	Mon Dec 20 16:44:33 2010 +0100
@@ -18,13 +18,13 @@
 
 typedecl tr
 typedecl void
-typedecl ('a,'b) "*"    (infixl "*" 6)
-typedecl ('a,'b) "+"    (infixl "+" 5)
+typedecl ('a,'b) prod  (infixl "*" 6)
+typedecl ('a,'b) sum  (infixl "+" 5)
 
 arities
   "fun" :: (cpo, cpo) cpo
-  "*" :: (cpo, cpo) cpo
-  "+" :: (cpo, cpo) cpo
+  prod :: (cpo, cpo) cpo
+  sum :: (cpo, cpo) cpo
   tr :: cpo
   void :: cpo