# HG changeset patch
# User wenzelm
# Date 1361653212 -3600
# Node ID 28b60ee75ef81133165d3856d86e3235ac9ab4f3
# Parent  93ccf48a46b75558e5f95ac262d4bac2bb3ccfbe
make SML/NJ happy;

diff -r 93ccf48a46b7 -r 28b60ee75ef8 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sat Feb 23 21:07:44 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sat Feb 23 22:00:12 2013 +0100
@@ -374,7 +374,7 @@
 
 val waldmeister_conjecture_num = "1.0.0.0"
 
-val repair_waldmeister_endgame =
+fun repair_waldmeister_endgame arg =
   let
     fun do_tail (name, _, t, rule, deps) =
       (name, Negated_Conjecture, s_not t, rule, deps)
@@ -382,7 +382,7 @@
       | do_body ((line as ((num, _), _, _, _, _)) :: lines) =
         if num = waldmeister_conjecture_num then map do_tail (line :: lines)
         else line :: do_body lines
-  in do_body end
+  in do_body arg end
 
 (* Recursively delete empty lines (type information) from the proof. *)
 fun add_nontrivial_line (line as (name, _, t, _, [])) lines =