changeset 23029 | 79ee75dc1e59 |
parent 22997 | d4f3b015b50b |
child 23075 | 69e30a7e8880 |
--- a/src/HOL/Tools/res_clause.ML Sat May 19 11:33:34 2007 +0200 +++ b/src/HOL/Tools/res_clause.ML Sat May 19 11:33:57 2007 +0200 @@ -117,7 +117,7 @@ ("op :", "in"), ("op Un", "union"), ("op Int", "inter"), - ("List.op @", "append"), + ("List.append", "append"), ("ATP_Linkup.fequal", "fequal"), ("ATP_Linkup.COMBI", "COMBI"), ("ATP_Linkup.COMBK", "COMBK"),