# HG changeset patch
# User smolkas
# Date 1354101943 -3600
# Node ID e8173d1fa725757584b50c30a7615984b430e891
# Parent  9eafa567e061728d799191bc83d3ce5bf8efbc87
removed duplicate decleration

diff -r 9eafa567e061 -r e8173d1fa725 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 ^ ")"