use regular Display.string_of_thm_global;

--- 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