direct instantiation unit :: discrete_cpo

--- a/src/HOLCF/Product_Cpo.thy	Fri Oct 22 06:58:45 2010 -0700
+++ b/src/HOLCF/Product_Cpo.thy	Fri Oct 22 07:44:34 2010 -0700
@@ -12,17 +12,16 @@
 
 subsection {* Unit type is a pcpo *}
 
-instantiation unit :: below
+instantiation unit :: discrete_cpo
 begin
 
 definition
   below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> True"
 
-instance ..
-end
+instance proof
+qed simp
 
-instance unit :: discrete_cpo
-by intro_classes simp
+end
 
 instance unit :: pcpo
 by intro_classes simp