diff -r efb95d0d01f7 -r e16da3068ad6 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Fri Mar 04 23:12:36 2005 +0100
+++ b/src/HOLCF/Cprod.thy	Fri Mar 04 23:23:47 2005 +0100
@@ -8,7 +8,9 @@
 
 header {* The cpo of cartesian products *}
 
-theory Cprod = Cfun:
+theory Cprod
+imports Cfun
+begin
 
 defaultsort cpo
 
@@ -231,7 +233,7 @@
   "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
 
 syntax (xsymbols)
-  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\\<Lambda>()<_>./ _)" [0, 10] 10)
+  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\<Lambda>()<_>./ _)" [0, 10] 10)
 
 (* for compatibility with old HOLCF-Version *)
 lemma inst_cprod_pcpo: "UU = (UU,UU)"