# HG changeset patch
# User blanchet
# Date 1304502586 -7200
# Node ID 223153bb68a1927dd5d4d771b3397090c937f4ff
# Parent  af86324707f2572a47c9334efd7111ca180d02e3
added type annotation for SML/NJ

diff -r af86324707f2 -r 223153bb68a1 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- 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})] @