src/HOLCF/Cprod.thy

--- a/src/HOLCF/Cprod.thy	Mon Jan 14 20:28:59 2008 +0100
+++ b/src/HOLCF/Cprod.thy	Mon Jan 14 20:35:52 2008 +0100
@@ -15,17 +15,16 @@
 
 subsection {* Type @{typ unit} is a pcpo *}
 
-instantiation unit :: sq_ord
+instantiation unit :: po
 begin
 
 definition
   less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
 
-instance ..
-end
+instance
+by intro_classes simp_all
 
-instance unit :: po
-by intro_classes simp_all
+end
 
 instance unit :: finite_po ..