--- a/src/HOL/Tools/res_clause.ML Thu Mar 05 08:23:10 2009 +0100
+++ b/src/HOL/Tools/res_clause.ML Thu Mar 05 08:23:11 2009 +0100
@@ -99,21 +99,21 @@
(*Provide readable names for the more common symbolic functions*)
val const_trans_table =
- Symtab.make [("op =", "equal"),
+ Symtab.make [(@{const_name "op ="}, "equal"),
(@{const_name HOL.less_eq}, "lessequals"),
(@{const_name HOL.less}, "less"),
- ("op &", "and"),
- ("op |", "or"),
+ (@{const_name "op &"}, "and"),
+ (@{const_name "op |"}, "or"),
(@{const_name HOL.plus}, "plus"),
(@{const_name HOL.minus}, "minus"),
(@{const_name HOL.times}, "times"),
(@{const_name Divides.div}, "div"),
(@{const_name HOL.divide}, "divide"),
- ("op -->", "implies"),
- ("{}", "emptyset"),
- ("op :", "in"),
- ("op Un", "union"),
- ("op Int", "inter"),
+ (@{const_name "op -->"}, "implies"),
+ (@{const_name Set.empty}, "emptyset"),
+ (@{const_name "op :"}, "in"),
+ (@{const_name Un}, "union"),
+ (@{const_name Int}, "inter"),
("List.append", "append"),
("ATP_Linkup.fequal", "fequal"),
("ATP_Linkup.COMBI", "COMBI"),