diff -r 39acf19e9f3a -r 30e2ffbba718 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 21 01:03:18 2009 +0200
@@ -655,7 +655,7 @@
                                   text=[XML.Elem("pgml",[],
                                                  maps YXML.parse_body strings)] })
 
-        fun string_of_thm th = Pretty.string_of (Display.pretty_thm_aux
+        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)