diff -r ebaa558fc698 -r 0e2679025aeb src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Mon Apr 26 09:26:31 2010 -0700
+++ b/src/HOL/SetInterval.thy	Mon Apr 26 09:37:46 2010 -0700
@@ -54,22 +54,22 @@
 @{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *}
 
 syntax
-  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3UN _<=_./ _)" 10)
-  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3UN _<_./ _)" 10)
-  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3INT _<=_./ _)" 10)
-  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" 10)
+  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3UN _<=_./ _)" [0, 0, 10] 10)
+  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3UN _<_./ _)" [0, 0, 10] 10)
+  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3INT _<=_./ _)" [0, 0, 10] 10)
+  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" [0, 0, 10] 10)
 
 syntax (xsymbols)
-  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" 10)
-  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _<_./ _)" 10)
-  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" 10)
-  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
+  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" [0, 0, 10] 10)
+  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _<_./ _)" [0, 0, 10] 10)
+  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" [0, 0, 10] 10)
+  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" [0, 0, 10] 10)
 
 syntax (latex output)
-  "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" 10)
-  "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" 10)
-  "_INTER_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" 10)
-  "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" 10)
+  "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" [0, 0, 10] 10)
+  "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" [0, 0, 10] 10)
+  "_INTER_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" [0, 0, 10] 10)
+  "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" [0, 0, 10] 10)
 
 translations
   "UN i<=n. A"  == "UN i:{..n}. A"