diff -r 304a47739407 -r 04ce6bb14d85 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Thu Sep 24 19:14:18 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Fri Sep 25 09:50:31 2009 +0200
@@ -74,8 +74,8 @@
         in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
           (p (fold (Logic.all o Var) vs t) f)
         end;
-      fun mkop "op &" T x = SOME (Const (@{const_name Set.inter}, T --> T --> T), x)
-        | mkop "op |" T x = SOME (Const (@{const_name Set.union}, T --> T --> T), x)
+      fun mkop "op &" T x = SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
+        | mkop "op |" T x = SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
         | mkop _ _ _ = NONE;
       fun mk_collect p T t =
         let val U = HOLogic.dest_setT T