# HG changeset patch
# User smolkas
# Date 1373456603 -7200
# Node ID e78ea835b5f8f957ebf9f2beab64c961f517aee4
# Parent  17138170ed7fa15dfdbef07681e3025d6ed59873
made SML/NJ happy

diff -r 17138170ed7f -r e78ea835b5f8 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Wed Jul 10 12:35:18 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Wed Jul 10 13:43:23 2013 +0200
@@ -231,8 +231,7 @@
                   (l, (fn () => preplay' preplay_timeout step) |> Lazy.lazy)
                   tab
             handle (exn as Canonical_Lbl_Tab.DUP _) =>
-              raise Fail ("Sledgehammer_Preplay: preplay time table - "
-                          ^ PolyML.makestring exn)
+              raise Fail "Sledgehammer_Preplay: preplay time table"
         in
           Canonical_Lbl_Tab.empty
           |> fold_isar_steps add_step_to_tab (steps_of_proof proof)