src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42675 223153bb68a1
parent 42674 af86324707f2
child 42677 25496cd3c199
--- 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})] @