diff -r ee143615019c -r f645b51e8e54 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Wed Jul 22 14:20:32 2009 +0200
+++ b/src/HOL/Tools/res_clause.ML	Wed Jul 22 14:20:32 2009 +0200
@@ -110,8 +110,8 @@
                    (@{const_name "op -->"}, "implies"),
                    (@{const_name Set.empty}, "emptyset"),
                    (@{const_name "op :"}, "in"),
-                   (@{const_name Un}, "union"),
-                   (@{const_name Int}, "inter"),
+                   (@{const_name union}, "union"),
+                   (@{const_name inter}, "inter"),
                    ("List.append", "append"),
                    ("ATP_Linkup.fequal", "fequal"),
                    ("ATP_Linkup.COMBI", "COMBI"),