--- a/src/HOL/Tools/SMT/z3_replay.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/SMT/z3_replay.ML Sat Mar 05 17:01:45 2016 +0100
@@ -72,7 +72,7 @@
val replay = Timing.timing (replay_thm ctxt assumed nthms)
val ({elapsed, ...}, thm) =
SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay step
- handle TimeLimit.TimeOut => raise SMT_Failure.SMT SMT_Failure.Time_Out
+ handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
val stats' = Symtab.cons_list (Z3_Proof.string_of_rule rule, Time.toMilliseconds elapsed) stats
in (Inttab.update (id, (fixes, thm)) proofs, stats') end