src/HOL/Tools/record_package.ML
changeset 8720 840c75ab2a7f
parent 8574 bed3b994ab26
child 9040 249c135057d7
     1.1 --- a/src/HOL/Tools/record_package.ML	Sat Apr 15 17:41:20 2000 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Mon Apr 17 13:57:55 2000 +0200
     1.3 @@ -379,7 +379,10 @@
     1.4        fun pretty_record (name, {args, parent, fields, simps = _}) = Pretty.block (Pretty.fbreaks
     1.5          (Pretty.block [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
     1.6            pretty_parent parent @ map pretty_field fields));
     1.7 -    in seq (Pretty.writeln o pretty_record) (Sign.cond_extern_table sg Sign.typeK recs) end;
     1.8 +    in
     1.9 +      map pretty_record (Sign.cond_extern_table sg Sign.typeK recs)
    1.10 +      |> Pretty.chunks |> Pretty.writeln
    1.11 +    end;
    1.12  end;
    1.13  
    1.14  structure RecordsData = TheoryDataFun(RecordsArgs);