src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

     | (pre, (name', _, _, _, _) :: post) =>
       line :: pre @ map (replace_dependencies_in_line (name', [name])) post
 
 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)
     fun do_body [] = []
       | 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 =
     if is_only_type_information t then delete_dependency name lines
     else line :: lines