--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Jul 18 08:44:04 2012 +0200
@@ -91,12 +91,6 @@
InternalError |
UnknownError of string
-fun elide_string threshold s =
- if size s > threshold then
- String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^
- String.extract (s, size s - (threshold + 1) div 2 + 6, NONE)
- else
- s
fun short_output verbose output =
if verbose then
if output = "" then "No details available" else elide_string 1000 output