1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 26 14:14:02 2009 +0100
1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 26 15:18:50 2009 +0100
1.3 @@ -655,13 +655,9 @@
1.4 text=[XML.Elem("pgml",[],
1.5 maps YXML.parse_body strings)] })
1.6
1.7 - fun string_of_thm th = Pretty.string_of
1.8 - (Display.pretty_thm_aux
1.9 - (Syntax.pp_global (Thm.theory_of_thm th))
1.10 - false (* quote *)
1.11 - false (* show hyps *)
1.12 - [] (* asms *)
1.13 - th)
1.14 + fun string_of_thm th = Pretty.string_of (Display.pretty_thm_aux
1.15 + (Syntax.pp_global (Thm.theory_of_thm th))
1.16 + {quote = false, show_hyps = false, show_status = true} [] th)
1.17
1.18 fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name)
1.19