src/Pure/ProofGeneral/proof_general_pgip.ML

         fun idvalue strings =
             issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
                                   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)
 
         fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name)