src/HOL/Tools/inductive_set.ML

       fun close p t f =
         let val vs = Term.add_vars t []
         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
         in HOLogic.Collect_const U $
           HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t