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