1.1 --- a/src/Pure/sign.ML	Tue Oct 09 00:20:13 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Oct 09 00:20:21 2007 +0200
     1.3 @@ -114,17 +114,12 @@
     1.4    val intern_term: theory -> term -> term
     1.5    val extern_term: (string -> xstring) -> theory -> term -> term
     1.6    val intern_tycons: theory -> typ -> typ
     1.7 -  val pretty_term': Proof.context -> Syntax.syntax -> (string -> xstring) -> term -> Pretty.T
     1.8    val pretty_term: theory -> term -> Pretty.T
     1.9    val pretty_typ: theory -> typ -> Pretty.T
    1.10    val pretty_sort: theory -> sort -> Pretty.T
    1.11 -  val pretty_classrel: theory -> class list -> Pretty.T
    1.12 -  val pretty_arity: theory -> arity -> Pretty.T
    1.13    val string_of_term: theory -> term -> string
    1.14    val string_of_typ: theory -> typ -> string
    1.15    val string_of_sort: theory -> sort -> string
    1.16 -  val string_of_classrel: theory -> class list -> string
    1.17 -  val string_of_arity: theory -> arity -> string
    1.18    val pp: theory -> Pretty.pp
    1.19    val arity_number: theory -> string -> int
    1.20    val arity_sorts: theory -> string -> sort -> sort list
    1.21 @@ -354,39 +349,21 @@
    1.22  
    1.23  (** pretty printing of terms, types etc. **)
    1.24  
    1.25 -fun pretty_term' ctxt syn ext t =
    1.26 -  let val curried = Context.exists_name Context.CPureN (ProofContext.theory_of ctxt)
    1.27 -  in Syntax.pretty_term ext ctxt syn curried t end;
    1.28 +val pretty_term = Syntax.pretty_term o ProofContext.init;
    1.29 +val pretty_typ = Syntax.pretty_typ o ProofContext.init;
    1.30 +val pretty_sort = Syntax.pretty_sort o ProofContext.init;
    1.31  
    1.32 -fun pretty_term thy t =
    1.33 -  pretty_term' (ProofContext.init thy) (syn_of thy) (Consts.extern (consts_of thy))
    1.34 -    (extern_term (Consts.extern_early (consts_of thy)) thy t);
    1.35 +val string_of_term = Syntax.string_of_term o ProofContext.init;
    1.36 +val string_of_typ = Syntax.string_of_typ o ProofContext.init;
    1.37 +val string_of_sort = Syntax.string_of_sort o ProofContext.init;
    1.38  
    1.39 -fun pretty_typ thy T =
    1.40 -  Syntax.pretty_typ (ProofContext.init thy) (syn_of thy) (extern_typ thy T);
    1.41 -
    1.42 -fun pretty_sort thy S =
    1.43 -  Syntax.pretty_sort (ProofContext.init thy) (syn_of thy) (extern_sort thy S);
    1.44 -
    1.45 -fun pretty_classrel thy cs = Pretty.block (flat
    1.46 -  (separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort thy o single) cs)));
    1.47 -
    1.48 -fun pretty_arity thy (a, Ss, S) =
    1.49 -  let
    1.50 -    val a' = extern_type thy a;
    1.51 -    val dom =
    1.52 -      if null Ss then []
    1.53 -      else [Pretty.list "(" ")" (map (pretty_sort thy) Ss), Pretty.brk 1];
    1.54 -  in Pretty.block ([Pretty.str (a' ^ " ::"), Pretty.brk 1] @ dom @ [pretty_sort thy S]) end;
    1.55 -
    1.56 -val string_of_term = Pretty.string_of oo pretty_term;
    1.57 -val string_of_typ = Pretty.string_of oo pretty_typ;
    1.58 -val string_of_sort = Pretty.string_of oo pretty_sort;
    1.59 -val string_of_classrel = Pretty.string_of oo pretty_classrel;
    1.60 -val string_of_arity = Pretty.string_of oo pretty_arity;
    1.61 -
    1.62 -fun pp thy = Pretty.pp (pretty_term thy, pretty_typ thy, pretty_sort thy,
    1.63 -  pretty_classrel thy, pretty_arity thy);
    1.64 +(*pp operations -- deferred evaluation*)
    1.65 +fun pp thy = Pretty.pp
    1.66 + (fn x => pretty_term thy x,
    1.67 +  fn x => pretty_typ thy x,
    1.68 +  fn x => pretty_sort thy x,
    1.69 +  fn x => Syntax.pretty_classrel (ProofContext.init thy) x,
    1.70 +  fn x => Syntax.pretty_arity (ProofContext.init thy) x);
    1.71  
    1.72  
    1.73