ThmDatabase.print_thms_containing;
authorwenzelm
Sun Sep 26 16:38:50 1999 +0200 (1999-09-26 ago)
changeset 7610c803ba5347fd
parent 7609 1acbed762fc6
child 7611 5b5aba10c8f6
ThmDatabase.print_thms_containing;
src/Pure/Interface/proof_general.ML
     1.1 --- a/src/Pure/Interface/proof_general.ML	Sun Sep 26 16:38:21 1999 +0200
     1.2 +++ b/src/Pure/Interface/proof_general.ML	Sun Sep 26 16:38:50 1999 +0200
     1.3 @@ -166,14 +166,7 @@
     1.4  
     1.5  (* some top-level commands for ProofGeneral/isa *)
     1.6  
     1.7 -fun prt_thm (a, th) =
     1.8 -  Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
     1.9 -    Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))];
    1.10 -
    1.11 -fun thms_containing cs =
    1.12 -  Pretty.blk (0, Pretty.fbreaks (map prt_thm (ThmDatabase.thms_containing cs)))
    1.13 -  |> Pretty.writeln;
    1.14 -
    1.15 +fun thms_containing cs = ThmDatabase.print_thms_containing (the_context ()) cs;
    1.16  
    1.17  val help = writeln o Session.welcome;
    1.18  val show_context = Context.the_context;