equal
deleted
inserted
replaced
391 Pretty.para |
391 Pretty.para |
392 (tool_name auto ^ " found a " ^ |
392 (tool_name auto ^ " found a " ^ |
393 (if genuine then "counterexample:" |
393 (if genuine then "counterexample:" |
394 else "potentially spurious counterexample due to underspecified functions:") ^ |
394 else "potentially spurious counterexample due to underspecified functions:") ^ |
395 Config.get ctxt tag); |
395 Config.get ctxt tag); |
396 val body = |
396 fun pretty_cex (x, t) = |
397 map (fn (s, t) => |
397 Pretty.block [Pretty.str (x ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]; |
398 Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex); |
|
399 in |
398 in |
400 Pretty.chunks (Pretty.block (Pretty.fbreaks (header :: body)) :: |
399 Pretty.chunks (Pretty.block (Pretty.fbreaks (header :: map pretty_cex (rev cex))) :: |
401 (if null eval_terms then [] |
400 (if null eval_terms then [] |
402 else |
401 else |
403 [Pretty.big_list "Evaluated terms:" |
402 [Pretty.big_list "Evaluated terms:" |
404 (map (fn (t, u) => |
403 (map (fn (t, u) => |
405 Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, |
404 Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, |