changeset 56334 | 6b3739fee456 |
parent 56245 | 84fc7dfa3cd4 |
child 58002 | 0ed1e999a0fb |
--- a/src/Tools/induct.ML Mon Mar 31 10:28:08 2014 +0200 +++ b/src/Tools/induct.ML Mon Mar 31 12:35:39 2014 +0200 @@ -254,7 +254,7 @@ pretty_rules ctxt "induct pred:" inductP, pretty_rules ctxt "cases type:" casesT, pretty_rules ctxt "cases pred:" casesP] - |> Pretty.chunks |> Pretty.writeln + |> Pretty.writeln_chunks end; val _ =