--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Tue Oct 26 11:39:26 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Tue Oct 26 11:45:12 2010 +0200
@@ -240,8 +240,8 @@
(* core parser *)
-fun parse_exn line_no msg = raise SMT_Solver.SMT ("Z3 proof parser (line " ^
- string_of_int line_no ^ "): " ^ msg)
+fun parse_exn line_no msg = raise SMT_Solver.SMT (SMT_Solver.Other_Failure
+ ("Z3 proof parser (line " ^ string_of_int line_no ^ "): " ^ msg))
fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg