# HG changeset patch
# User paulson
# Date 1134484442 -3600
# Node ID aaecdaef4c042a1ec301cca34906dbb67096b216
# Parent  8352b1d3b6399cf6eea1524583a50dd4207dac05
now generates the name "append"

diff -r 8352b1d3b639 -r aaecdaef4c04 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Tue Dec 13 15:27:43 2005 +0100
+++ b/src/HOL/Tools/res_clause.ML	Tue Dec 13 15:34:02 2005 +0100
@@ -113,7 +113,8 @@
 		   ("{}", "emptyset"),
 		   ("op :", "in"),
 		   ("op Un", "union"),
-		   ("op Int", "inter")];
+		   ("op Int", "inter"),
+		   ("List.op @", "append")];
 
 val type_const_trans_table =
       Symtab.make [("*", "t_prod"),