# HG changeset patch
# User wenzelm
# Date 1248360211 -7200
# Node ID 183c1010ac141bfca31b8e6cc916f78b6c8d13e1
# Parent  6e4eb80e4a8cecea14dad6a5ae6257c46c0fe953
use regular Display.string_of_thm_global;

diff -r 6e4eb80e4a8c -r 183c1010ac14 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Jul 23 16:09:50 2009 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Jul 23 16:43:31 2009 +0200
@@ -655,11 +655,8 @@
                                   text=[XML.Elem("pgml",[],
                                                  maps YXML.parse_body strings)] })
 
-        fun string_of_thm th = Pretty.string_of (Display.pretty_thm_raw
-            (Syntax.pp_global (Thm.theory_of_thm th))
-            {quote = false, show_hyps = false, show_status = true} [] th)
-
-        fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name)
+        fun strings_of_thm (thy, name) =
+          map (Display.string_of_thm_global thy) (PureThy.get_thms thy name)
 
         val string_of_thy = Pretty.string_of o ProofDisplay.pretty_full_theory false
     in