src/Pure/Isar/isar_cmd.ML
changeset 33388 d64545e6cba5
parent 33369 470a7b233ee5
child 33389 bb3a5fa94a91
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Nov 02 20:48:08 2009 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Nov 02 20:50:48 2009 +0100
     1.3 @@ -460,11 +460,11 @@
     1.4            val prop = Thm.full_prop_of thm;
     1.5            val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
     1.6          in
     1.7 -          ProofSyntax.pretty_proof ctxt
     1.8 +          Proof_Syntax.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 (ProofSyntax.pretty_proof_of (Proof.context_of state) full)
    1.13 +        (map (Proof_Syntax.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 =