# HG changeset patch
# User blanchet
# Date 1272463429 -7200
# Node ID a3357a631b9695c22f2c8e51e389152041620ecb
# Parent  60532b9bcd1c22e3268afb458566f92766859bdb
reintroduced short names for HOL->FOL constants; other parts of the code rely on these

diff -r 60532b9bcd1c -r a3357a631b96 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Apr 28 15:53:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Apr 28 16:03:49 2010 +0200
@@ -107,13 +107,20 @@
 
 fun union_all xss = fold (union (op =)) xss []
 
-(* Provide readable names for the more common symbolic functions *)
+(* Readable names for the more common symbolic functions. Do not mess with the
+   last six entries of the table unless you know what you are doing. *)
 val const_trans_table =
   Symtab.make [(@{const_name "op ="}, "equal"),
                (@{const_name "op &"}, "and"),
                (@{const_name "op |"}, "or"),
                (@{const_name "op -->"}, "implies"),
-               (@{const_name "op :"}, "in")]
+               (@{const_name "op :"}, "in"),
+               (@{const_name fequal}, "fequal"),
+               (@{const_name COMBI}, "COMBI"),
+               (@{const_name COMBK}, "COMBK"),
+               (@{const_name COMBB}, "COMBB"),
+               (@{const_name COMBC}, "COMBC"),
+               (@{const_name COMBS}, "COMBS")]
 
 val type_const_trans_table =
   Symtab.make [(@{type_name "*"}, "prod"),