src/HOL/Tools/res_clause.ML
changeset 32135 f645b51e8e54
parent 31910 a8e9ccfc427a
child 32264 0be31453f698
--- 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"),