added print_thm(s)_sg;
authorwenzelm
Sun Sep 17 22:23:48 2000 +0200 (2000-09-17)
changeset 10010f6ccb6df9cb9
parent 10009 45c1eb3d8ad4
child 10011 ed5262aee27f
added print_thm(s)_sg;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Sun Sep 17 22:22:11 2000 +0200
     1.2 +++ b/src/Pure/display.ML	Sun Sep 17 22:23:48 2000 +0200
     1.3 @@ -13,6 +13,8 @@
     1.4    val pretty_thm_no_quote: thm -> Pretty.T
     1.5    val pretty_thm	: thm -> Pretty.T
     1.6    val pretty_thms	: thm list -> Pretty.T
     1.7 +  val pretty_thm_sg     : Sign.sg -> thm -> Pretty.T
     1.8 +  val pretty_thms_sg    : Sign.sg -> thm list -> Pretty.T
     1.9    val string_of_thm	: thm -> string
    1.10    val pprint_thm	: thm -> pprint_args -> unit
    1.11    val print_thm		: thm -> unit
    1.12 @@ -85,6 +87,9 @@
    1.13  fun pretty_thms [th] = pretty_thm th
    1.14    | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
    1.15  
    1.16 +val pretty_thm_sg = pretty_thm oo Thm.transfer_sg;
    1.17 +val pretty_thms_sg = pretty_thms oo (map o Thm.transfer_sg);
    1.18 +
    1.19  
    1.20  (* top-level commands for printing theorems *)
    1.21