# HG changeset patch
# User wenzelm
# Date 880036237 -3600
# Node ID f2ca5a87f0a7ef31677318fe844efeb0329a79c1
# Parent  1663f9056045afefebc54bbb6eb864c5398bb36d
improved theorems print method: transfer_sg;

diff -r 1663f9056045 -r f2ca5a87f0a7 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Nov 20 15:30:03 1997 +0100
+++ b/src/Pure/pure_thy.ML	Thu Nov 20 15:30:37 1997 +0100
@@ -52,9 +52,9 @@
   Theorems (ref {space = NameSpace.empty,
     thms_tab = Symtab.null, const_idx = (0, Symtab.null)});
 
-fun print (Theorems (ref {space, thms_tab, const_idx = _})) =
+fun print sg (Theorems (ref {space, thms_tab, const_idx = _})) =
   let
-    val prt_thm = Pretty.quote o Display.pretty_thm;
+    val prt_thm = Pretty.quote o Display.pretty_thm o Thm.transfer_sg sg;
     fun prt_thms (name, [th]) =
           Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th]
       | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
@@ -70,7 +70,7 @@
 in
 
 val theorems_data: string * (object * (object -> object) *
-  (object * object -> object) * (object -> unit)) =
+  (object * object -> object) * (Sign.sg -> object -> unit)) =
     (theoremsK, (mk_empty (), mk_empty, mk_empty, print));
 
 end;