| changeset 19 | 929ad32d63fc |
| parent 0 | a5a9c433f639 |
| child 58 | b30802dfbe80 |
--- a/src/Pure/POLY.ML Mon Oct 04 15:30:49 1993 +0100 +++ b/src/Pure/POLY.ML Mon Oct 04 15:36:31 1993 +0100 @@ -32,7 +32,8 @@ (*Interface for toplevel pretty printers, see also Pure/install_pp.ML*) fun make_pp _ pprint (str, blk, brk, en) obj = - pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0), en); + pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0), + fn () => brk (99999, 0), en); (*** File information ***)