src/Pure/Thy/thy_output.ML
changeset 42359 6ca5407863ed
parent 42358 b47d41d9f4b5
child 42360 da8817d01e7c
     1.1 --- a/src/Pure/Thy/thy_output.ML	Sat Apr 16 13:48:45 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Apr 16 15:25:25 2011 +0200
     1.3 @@ -510,11 +510,11 @@
     1.4    in ProofContext.pretty_term_abbrev ctxt' eq end;
     1.5  
     1.6  fun pretty_class ctxt =
     1.7 -  Pretty.str o Type.extern_class ctxt (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt;
     1.8 +  Pretty.str o ProofContext.extern_class ctxt o ProofContext.read_class ctxt;
     1.9  
    1.10  fun pretty_type ctxt s =
    1.11    let val Type (name, _) = ProofContext.read_type_name_proper ctxt false s
    1.12 -  in Pretty.str (Type.extern_type ctxt (ProofContext.tsig_of ctxt) name) end;
    1.13 +  in Pretty.str (ProofContext.extern_type ctxt name) end;
    1.14  
    1.15  fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
    1.16