src/HOLCF/SetPcpo.thy

--- a/src/HOLCF/SetPcpo.thy	Mon Jan 14 03:54:31 2008 +0100
+++ b/src/HOLCF/SetPcpo.thy	Mon Jan 14 03:56:31 2008 +0100
@@ -9,17 +9,16 @@
 imports Adm
 begin
 
-instantiation set :: (type) sq_ord
+instantiation set :: (type) po
 begin
 
 definition
   less_set_def: "(op \<sqsubseteq>) = (op \<subseteq>)"
 
-instance ..
-end
+instance
+by (intro_classes, auto simp add: less_set_def)
 
-instance set :: (type) po
-by (intro_classes, auto simp add: less_set_def)
+end
 
 instance set :: (finite) finite_po ..