# HG changeset patch
# User blanchet
# Date 1387381814 -3600
# Node ID 9ce867291c76330f48759402265375520e941544
# Parent  6b65d1a45671067c7ee31480c8b8b49495955edd
made SML/NJ happier

diff -r 6b65d1a45671 -r 9ce867291c76 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Dec 18 16:50:14 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Dec 18 16:50:14 2013 +0100
@@ -658,7 +658,7 @@
 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
 
 val spass_pirate_format = DFG Polymorphic
-val remote_spass_pirate_config =
+val remote_spass_pirate_config : atp_config =
   {exec = K (["ISABELLE_ATP"], ["scripts/remote_spass_pirate"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
      string_of_int (to_secs 1 timeout) ^ " " ^ file_name,