equal
deleted
inserted
replaced
469 of SOME (bind, t') => let |
469 of SOME (bind, t') => let |
470 val (binds, t'') = implode_monad t' |
470 val (binds, t'') = implode_monad t' |
471 val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term) |
471 val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term) |
472 (bind :: binds) vars; |
472 (bind :: binds) vars; |
473 in |
473 in |
474 (brackify fxy o single o enclose "do { " " }" o Pretty.breaks) |
474 brackify_block fxy (str "do { ") |
475 (ps @| print_term vars' NOBR t'') |
475 (ps @| print_term vars' NOBR t'') |
|
476 (str " }") |
476 end |
477 end |
477 | NONE => brackify_infix (1, L) fxy |
478 | NONE => brackify_infix (1, L) fxy |
478 (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2) |
479 (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2) |
479 in (2, pretty) end; |
480 in (2, pretty) end; |
480 |
481 |