# 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"),