src/HOL/Tools/inductive_package.ML
changeset 8720 840c75ab2a7f
parent 8634 3f34637cb9c0
child 9072 a4896cf23638
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Apr 15 17:41:20 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Apr 17 13:57:55 2000 +0200
     1.3 @@ -79,9 +79,9 @@
     1.4      Library.generic_merge Thm.eq_thm I I monos1 monos2);
     1.5  
     1.6    fun print sg (tab, monos) =
     1.7 -    (Pretty.writeln (Pretty.strs ("(co)inductives:" ::
     1.8 -       map #1 (Sign.cond_extern_table sg Sign.constK tab)));
     1.9 -     Pretty.writeln (Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)));
    1.10 +    [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
    1.11 +     Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)]
    1.12 +    |> Pretty.chunks |> Pretty.writeln;
    1.13  end;
    1.14  
    1.15  structure InductiveData = TheoryDataFun(InductiveArgs);