diff -r 1f5b5dc3f48a -r 77ca20b0ed77 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -40,7 +40,7 @@
   "insert"  ("(_ ins _)")
   "op Un"   ("(_ union _)")
   "op Int"  ("(_ inter _)")
-  "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("(_ \\\\ _)")
+  "HOL.minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("(_ \\\\ _)")
   "image"   ("\<module>image")
 attach {*
 fun image f S = distinct (map f S);