diff -r e1eedc8cad37 -r b8d6c395c9e2 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat May 01 22:01:57 2004 +0200
+++ b/src/HOL/Set.thy	Sat May 01 22:04:14 2004 +0200
@@ -41,8 +41,7 @@
 
 local
 
-instance set :: (type) ord ..
-instance set :: (type) minus ..
+instance set :: (type) "{ord, minus}" ..
 
 
 subsection {* Additional concrete syntax *}
@@ -129,10 +128,10 @@
   "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" 10)
 
 syntax (xsymbols)
-  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>\<^bsub>_\<^esub>/ _)" 10)
-  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>\<^bsub>_\<^esub>/ _)" 10)
-  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>\<^bsub>_\<in>_\<^esub>/ _)" 10)
-  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>\<^bsub>_\<in>_\<^esub>/ _)" 10)
+  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>()\<^bsub>_\<^esub>/ _)" 10)
+  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>()\<^bsub>_\<^esub>/ _)" 10)
+  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>()\<^bsub>_\<in>_\<^esub>/ _)" 10)
+  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>()\<^bsub>_\<in>_\<^esub>/ _)" 10)
 
 
 translations