be more discriminate: some one-line Isar proofs are silly
(* Title: Pure/ML-Systems/ml_pretty.ML Author: MakariusRaw datatype for ML pretty printing.*)structure ML_Pretty =structdatatype pretty = Block of (string * string) * pretty list * int | String of string * int | Break of bool * int;end;