diff -r 82cceaf768c8 -r 466599ecf610 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Sun May 06 18:07:06 2007 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Sun May 06 21:49:23 2007 +0200
@@ -347,7 +347,7 @@
   "insert"  ("{*insertl*}")
   "op Un"   ("{*unionl*}")
   "op Int"  ("{*intersect*}")
-  "HOL.minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+  "minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
             ("{*flip subtract*}")
   "image"   ("{*map_distinct*}")
   "Union"   ("{*unions*}")