equal
deleted
inserted
replaced
238 fun finish (_, _, _, steps, vars, ctxt) = (steps, vars, ctxt) |
238 fun finish (_, _, _, steps, vars, ctxt) = (steps, vars, ctxt) |
239 |
239 |
240 |
240 |
241 (* core parser *) |
241 (* core parser *) |
242 |
242 |
243 fun parse_exn line_no msg = raise SMT_Solver.SMT ("Z3 proof parser (line " ^ |
243 fun parse_exn line_no msg = raise SMT_Solver.SMT (SMT_Solver.Other_Failure |
244 string_of_int line_no ^ "): " ^ msg) |
244 ("Z3 proof parser (line " ^ string_of_int line_no ^ "): " ^ msg)) |
245 |
245 |
246 fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg |
246 fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg |
247 |
247 |
248 fun with_info f cx = |
248 fun with_info f cx = |
249 (case f ((NONE, 1), cx) of |
249 (case f ((NONE, 1), cx) of |