src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 30726 a3adc9a96a16
parent 30364 577edc39b501
child 31478 5e412e4c6546
     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