author | smolkas |
Wed, 28 Nov 2012 12:25:43 +0100 | |
changeset 50266 | e8173d1fa725 |
parent 50265 | 9eafa567e061 |
child 50267 | 1da2e67242d6 |
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML | file | annotate | diff | comparison | revisions |
--- 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 ^ ")"