src/Pure/Thy/thy_output.ML
changeset 27258 656cfac246be
parent 26996 090a619e7d87
child 27344 d44490b06190
     1.1 --- a/src/Pure/Thy/thy_output.ML	Wed Jun 18 18:55:05 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Jun 18 18:55:06 2008 +0200
     1.3 @@ -479,7 +479,7 @@
     1.4    pretty_term_style ctxt (name, Thm.full_prop_of th);
     1.5  
     1.6  fun pretty_prf full ctxt thms =
     1.7 -  Pretty.chunks (map (ProofContext.pretty_proof_of ctxt full) thms);
     1.8 +  Pretty.chunks (map (ProofSyntax.pretty_proof_of ctxt full) thms);
     1.9  
    1.10  fun pretty_theory ctxt name =
    1.11    (Theory.requires (ProofContext.theory_of ctxt) name "presentation"; Pretty.str name);