thms_containing: single writeln;
authorwenzelm
Wed Sep 22 21:49:37 1999 +0200 (1999-09-22 ago)
changeset 758118070ae7a84c
parent 7580 536499cf71af
child 7582 2650c9c2ab7f
thms_containing: single writeln;
src/Pure/Interface/proof_general.ML
     1.1 --- a/src/Pure/Interface/proof_general.ML	Wed Sep 22 21:45:35 1999 +0200
     1.2 +++ b/src/Pure/Interface/proof_general.ML	Wed Sep 22 21:49:37 1999 +0200
     1.3 @@ -160,11 +160,14 @@
     1.4  
     1.5  (* some top-level commands for ProofGeneral/isa *)
     1.6  
     1.7 -fun print_thm (a, th) =
     1.8 -  Pretty.writeln (Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
     1.9 -    Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))]);
    1.10 +fun prt_thm (a, th) =
    1.11 +  Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
    1.12 +    Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))];
    1.13  
    1.14 -val thms_containing = seq print_thm o ThmDatabase.thms_containing;
    1.15 +fun thms_containing cs =
    1.16 +  Pretty.blk (0, Pretty.fbreaks (map prt_thm (ThmDatabase.thms_containing cs)))
    1.17 +  |> Pretty.writeln;
    1.18 +
    1.19  
    1.20  val help = writeln o Session.welcome;
    1.21  val show_context = Context.the_context;