(* Moscow ML pretty printing *) open PP ; val strlr = ref [] : string list ref ; val strr = ref "" ; fun push str = strlr := str :: (!strlr) ; fun flush () = (strr := String.concat (rev (!strlr)) ; strlr := []) ; val ppstrm = mk_ppstream {consumer = push, flush = flush, linewidth = 50} ; pp_thm ppstrm AND_CLAUSES ; flush_ppstream ppstrm ; print (!strr) ;