--- a/src/HOL/Tools/inductive_set.ML Fri Sep 18 14:09:38 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML Sat Sep 19 07:38:03 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