# HG changeset patch
# User mengj
# Date 1159619501 -7200
# Node ID a9595fdc02b1bfb6d13b6d5b479ab5578a427139
# Parent  e279499c4f803c3b2cde7d5811a663bb62596e8b
Added the combinator constants to the constants table.

diff -r e279499c4f80 -r a9595fdc02b1 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Sat Sep 30 14:31:02 2006 +0200
+++ b/src/HOL/Tools/res_clause.ML	Sat Sep 30 14:31:41 2006 +0200
@@ -118,7 +118,16 @@
 		   ("op :", "in"),
 		   ("op Un", "union"),
 		   ("op Int", "inter"),
-		   ("List.op @", "append")];
+		   ("List.op @", "append"),
+		   ("Reconstruction.fequal", "fequal"),
+		   ("Reconstruction.COMBI", "COMBI"),
+		   ("Reconstruction.COMBK", "COMBK"),
+		   ("Reconstruction.COMBB", "COMBB"),
+		   ("Reconstruction.COMBC", "COMBC"),
+		   ("Reconstruction.COMBS", "COMBS"),
+		   ("Reconstruction.COMBB'", "COMBB_e"),
+		   ("Reconstruction.COMBC'", "COMBC_e"),
+		   ("Reconstruction.COMBS'", "COMBS_e")];
 
 val type_const_trans_table =
       Symtab.make [("*", "prod"),