diff -r ee143615019c -r f645b51e8e54 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Wed Jul 22 14:20:32 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Wed Jul 22 14:20:32 2009 +0200
@@ -73,8 +73,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 "Int"}, T --> T --> T), x)
-        | mkop "op |" T x = SOME (Const (@{const_name "Un"}, T --> T --> T), x)
+      fun mkop "op &" T x = SOME (Const (@{const_name inter}, T --> T --> T), x)
+        | mkop "op |" T x = SOME (Const (@{const_name union}, T --> T --> T), x)
         | mkop _ _ _ = NONE;
       fun mk_collect p T t =
         let val U = HOLogic.dest_setT T