removed duplicate decleration
authorsmolkas
Wed, 28 Nov 2012 12:25:43 +0100
changeset 50266 e8173d1fa725
parent 50265 9eafa567e061
child 50267 1da2e67242d6
removed duplicate decleration
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 28 12:25:43 2012 +0100
@@ -204,8 +204,6 @@
 
 (** 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 ^ ")"