removed obsolete pprint operations;
some explicit pp operations for toplevel pretty printing;

--- a/src/Pure/Isar/proof_context.ML	Sat Mar 21 20:00:23 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Mar 21 20:00:23 2009 +0100
@@ -36,7 +36,6 @@
   val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
   val extern_fact: Proof.context -> string -> xstring
   val pretty_term_abbrev: Proof.context -> term -> Pretty.T
-  val pretty_thm_legacy: thm -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
   val pretty_thms: Proof.context -> thm list -> Pretty.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
@@ -296,10 +295,6 @@
 
 fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
 
-fun pretty_thm_legacy th =
-  let val thy = Thm.theory_of_thm th
-  in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
-
 fun pretty_thm ctxt th =
   let val asms = map Thm.term_of (Assumption.all_assms_of ctxt)
   in Display.pretty_thm_aux (Syntax.pp ctxt) false true asms th end;

--- a/src/Pure/Isar/proof_display.ML	Sat Mar 21 20:00:23 2009 +0100
+++ b/src/Pure/Isar/proof_display.ML	Sat Mar 21 20:00:23 2009 +0100
@@ -6,12 +6,12 @@
 
 signature PROOF_DISPLAY =
 sig
-  val pprint_context: Proof.context -> pprint_args -> unit
-  val pprint_typ: theory -> typ -> pprint_args -> unit
-  val pprint_term: theory -> term -> pprint_args -> unit
-  val pprint_ctyp: ctyp -> pprint_args -> unit
-  val pprint_cterm: cterm -> pprint_args -> unit
-  val pprint_thm: thm -> pprint_args -> unit
+  val pp_context: Proof.context -> Pretty.T
+  val pp_thm: thm -> Pretty.T
+  val pp_typ: theory -> typ -> Pretty.T
+  val pp_term: theory -> term -> Pretty.T
+  val pp_ctyp: ctyp -> Pretty.T
+  val pp_cterm: cterm -> Pretty.T
   val print_theorems_diff: theory -> theory -> unit
   val print_theorems: theory -> unit
   val pretty_full_theory: bool -> theory -> Pretty.T
@@ -26,18 +26,20 @@
 
 (* toplevel pretty printing *)
 
-fun pprint_context ctxt = Pretty.pprint
+fun pp_context ctxt =
  (if ! ProofContext.debug then
     Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
   else Pretty.str "<context>");
 
-fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (Syntax.init_pretty_global thy);
+fun pp_thm th =
+  let val thy = Thm.theory_of_thm th
+  in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
 
-val pprint_typ = pprint Syntax.pretty_typ;
-val pprint_term = pprint Syntax.pretty_term;
-fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
-fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
-val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
+val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
+val pp_term = Pretty.quote oo Syntax.pretty_term_global;
+
+fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
+fun pp_cterm ct = pp_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
 
 
 (* theorems and theory *)

--- a/src/Pure/Syntax/ast.ML	Sat Mar 21 20:00:23 2009 +0100
+++ b/src/Pure/Syntax/ast.ML	Sat Mar 21 20:00:23 2009 +0100
@@ -20,7 +20,6 @@
   val str_of_ast: ast -> string
   val pretty_ast: ast -> Pretty.T
   val pretty_rule: ast * ast -> Pretty.T
-  val pprint_ast: ast -> pprint_args -> unit
   val fold_ast: string -> ast list -> ast
   val fold_ast_p: string -> ast list * ast -> ast
   val unfold_ast: string -> ast -> ast list
@@ -79,8 +78,6 @@
   | pretty_ast (Appl asts) =
       Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
 
-val pprint_ast = Pretty.pprint o pretty_ast;
-
 fun pretty_rule (lhs, rhs) =
   Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
 

--- a/src/Pure/context.ML	Sat Mar 21 20:00:23 2009 +0100
+++ b/src/Pure/context.ML	Sat Mar 21 20:00:23 2009 +0100
@@ -27,8 +27,6 @@
   val display_names: theory -> string list
   val pretty_thy: theory -> Pretty.T
   val string_of_thy: theory -> string
-  val pprint_thy: theory -> pprint_args -> unit
-  val pprint_thy_ref: theory_ref -> pprint_args -> unit
   val pretty_abbrev_thy: theory -> Pretty.T
   val str_of_thy: theory -> string
   val deref: theory_ref -> theory
@@ -228,7 +226,6 @@
 
 val pretty_thy = Pretty.str_list "{" "}" o display_names;
 val string_of_thy = Pretty.string_of o pretty_thy;
-val pprint_thy = Pretty.pprint o pretty_thy;
 
 fun pretty_abbrev_thy thy =
   let
@@ -256,8 +253,6 @@
     else thy_ref
   end;
 
-val pprint_thy_ref = Pretty.pprint o pretty_thy o deref;
-
 
 (* build ids *)