moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
authorwenzelm
Wed Jun 18 18:55:06 2008 +0200 (2008-06-18)
changeset 27258656cfac246be
parent 27257 ddc00dbad26b
child 27259 6e71abb8c994
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
src/Pure/Isar/isar_cmd.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Jun 18 18:55:05 2008 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Jun 18 18:55:06 2008 +0200
     1.3 @@ -584,11 +584,11 @@
     1.4            val prop = Thm.full_prop_of thm;
     1.5            val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
     1.6          in
     1.7 -          ProofContext.pretty_proof ctxt
     1.8 +          ProofSyntax.pretty_proof ctxt
     1.9              (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
    1.10          end
    1.11      | SOME args => Pretty.chunks
    1.12 -        (map (ProofContext.pretty_proof_of (Proof.context_of state) full)
    1.13 +        (map (ProofSyntax.pretty_proof_of (Proof.context_of state) full)
    1.14            (Proof.get_thmss state args)));
    1.15  
    1.16  fun string_of_prop state s =
     2.1 --- a/src/Pure/Thy/thy_output.ML	Wed Jun 18 18:55:05 2008 +0200
     2.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Jun 18 18:55:06 2008 +0200
     2.3 @@ -479,7 +479,7 @@
     2.4    pretty_term_style ctxt (name, Thm.full_prop_of th);
     2.5  
     2.6  fun pretty_prf full ctxt thms =
     2.7 -  Pretty.chunks (map (ProofContext.pretty_proof_of ctxt full) thms);
     2.8 +  Pretty.chunks (map (ProofSyntax.pretty_proof_of ctxt full) thms);
     2.9  
    2.10  fun pretty_theory ctxt name =
    2.11    (Theory.requires (ProofContext.theory_of ctxt) name "presentation"; Pretty.str name);