--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Mar 27 13:00:40 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Mar 27 17:12:40 2014 +0100
@@ -160,7 +160,7 @@
if Exn.is_interrupt exn orelse debug then
reraise exn
else
- {outcome = SOME (SMT2_Failure.Other_Failure (ML_Compiler.exn_message exn)),
+ {outcome = SOME (SMT2_Failure.Other_Failure (Runtime.exn_message exn)),
rewrite_rules = [], conjecture_id = ~1, helper_ids = [], fact_ids = [],
z3_proof = []}