| 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 ^ ")"