diff -r 0dbcb73bf9bf -r 475ff421a6a3 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Thu May 10 10:21:50 2007 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Thu May 10 10:22:17 2007 +0200
@@ -343,19 +343,18 @@
 subsubsection {* const serializations *}
 
 consts_code
-  "{}"      ("[]")
-  "insert"  ("{*insertl*}")
-  "op Un"   ("{*unionl*}")
-  "op Int"  ("{*intersect*}")
-  "minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
-            ("{*flip subtract*}")
-  "image"   ("{*map_distinct*}")
-  "Union"   ("{*unions*}")
-  "Inter"   ("{*intersects*}")
-  "UNION"   ("{*map_union*}")
-  "INTER"   ("{*map_inter*}")
-  "Ball"    ("{*Blall*}")
-  "Bex"     ("{*Blex*}")
-  "filter_set" ("{*filter*}")
+  "{}" ("{*[]*}")
+  insert ("{*insertl*}")
+  "op \<union>" ("{*unionl*}")
+  "op \<inter>" ("{*intersect*}")
+  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}")
+  image ("{*map_distinct*}")
+  Union ("{*unions*}")
+  Inter ("{*intersects*}")
+  UNION ("{*map_union*}")
+  INTER ("{*map_inter*}")
+  Ball ("{*Blall*}")
+  Bex ("{*Blex*}")
+  filter_set ("{*filter*}")
 
 end