diff -r 2754a0dadccc -r 55edadbd43d5 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Thu Jun 04 15:28:59 2009 +0200
+++ b/src/HOL/Tools/hologic.ML	Thu Jun 04 15:28:59 2009 +0200
@@ -152,13 +152,13 @@
   let
     val sT = mk_setT T;
     val empty = Const ("Set.empty", sT);
-    fun insert t u = Const ("insert", T --> sT --> sT) $ t $ u;
+    fun insert t u = Const ("Set.insert", T --> sT --> sT) $ t $ u;
   in fold_rev insert ts empty end;
 
 fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
 
-fun dest_set (Const ("Orderings.bot", _)) = []
-  | dest_set (Const ("insert", _) $ t $ u) = t :: dest_set u
+fun dest_set (Const ("Set.empty", _)) = []
+  | dest_set (Const ("Set.insert", _) $ t $ u) = t :: dest_set u
   | dest_set t = raise TERM ("dest_set", [t]);
 
 fun Collect_const T = Const ("Collect", (T --> boolT) --> mk_setT T);