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