# HG changeset patch
# User blanchet
# Date 1387457202 -3600
# Node ID e1da23db35a9025342dbaf3b3317c8ad72fd3b7c
# Parent  10d48c2a3e320ede7fcc960c6d42e139aa32c0cf
made SML/NJ-friendlier (hopefully)

diff -r 10d48c2a3e32 -r e1da23db35a9 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Dec 19 13:43:21 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Dec 19 13:46:42 2013 +0100
@@ -149,12 +149,12 @@
       val ctxt' = ctxt
         |> debug ? (Config.put Metis_Tactic.verbose true #> Config.put Lin_Arith.verbose true)
 
-      val prove = Goal.prove ctxt' [] [] goal
+      fun prove () =
+        Goal.prove ctxt' [] [] goal (fn {context = ctxt, ...} =>
+          HEADGOAL (tac_of_method meth type_enc lam_trans ctxt facts))
+        handle ERROR msg => error ("Preplay error: " ^ msg)
 
-      fun tac {context = ctxt, ...} = HEADGOAL (tac_of_method meth type_enc lam_trans ctxt facts)
-      fun run_tac () = prove tac handle ERROR msg => error ("Preplay error: " ^ msg)
-
-      val preplay_time = take_time timeout run_tac ()
+      val preplay_time = take_time timeout prove ()
     in
       (if Config.get ctxt trace then preplay_trace ctxt facts goal preplay_time else ();
        preplay_time)