# HG changeset patch
# User wenzelm
# Date 969222228 -7200
# Node ID f6ccb6df9cb964e728c8d5a5a8035bd6991db4bb
# Parent  45c1eb3d8ad4073581c8563a4082ea7490b99628
added print_thm(s)_sg;

diff -r 45c1eb3d8ad4 -r f6ccb6df9cb9 src/Pure/display.ML
--- a/src/Pure/display.ML	Sun Sep 17 22:22:11 2000 +0200
+++ b/src/Pure/display.ML	Sun Sep 17 22:23:48 2000 +0200
@@ -13,6 +13,8 @@
   val pretty_thm_no_quote: thm -> Pretty.T
   val pretty_thm	: thm -> Pretty.T
   val pretty_thms	: thm list -> Pretty.T
+  val pretty_thm_sg     : Sign.sg -> thm -> Pretty.T
+  val pretty_thms_sg    : Sign.sg -> thm list -> Pretty.T
   val string_of_thm	: thm -> string
   val pprint_thm	: thm -> pprint_args -> unit
   val print_thm		: thm -> unit
@@ -85,6 +87,9 @@
 fun pretty_thms [th] = pretty_thm th
   | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
 
+val pretty_thm_sg = pretty_thm oo Thm.transfer_sg;
+val pretty_thms_sg = pretty_thms oo (map o Thm.transfer_sg);
+
 
 (* top-level commands for printing theorems *)