--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed May 04 10:12:44 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed May 04 11:49:46 2011 +0200
@@ -477,7 +477,7 @@
fun add_fact_syms_to_table explicit_apply =
fact_lift (formula_fold (add_combterm_syms_to_table explicit_apply))
-val default_sym_table_entries =
+val default_sym_table_entries : (string * sym_info) list =
[("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
(make_fixed_const predicator_base,
{pred_sym = true, min_ary = 1, max_ary = 1, typ = NONE})] @