src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

         NONE
     end
 
 
 (** one-liner reconstructor proofs **)
-
-fun string_for_label (s, num) = s ^ string_of_int num
 
 fun show_time NONE = ""
   | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")"
 
 (* FIXME: Various bugs, esp. with "unfolding"