pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;

--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Sep 04 22:36:42 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Sep 05 19:47:40 2010 +0200
@@ -315,7 +315,6 @@
 (* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
 fun mutate_theorem create_entry thy mtds thm =
   let
-    val pp = Syntax.pp_global thy
     val exec = is_executable_thm thy thm
     val _ = priority (if exec then "EXEC" else "NOEXEC")
     val mutants =
@@ -343,7 +342,7 @@
           |> map Mutabelle.freeze |> map freezeT
 (*          |> filter (not o is_forbidden_mutant) *)
           |> List.mapPartial (try (Sign.cert_term thy))
-    val _ = map (fn t => priority ("MUTANT: " ^ Pretty.string_of (Pretty.term pp t))) mutants
+    val _ = map (fn t => priority ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
   in
     create_entry thy thm exec mutants mtds
   end

--- a/src/Pure/Isar/class.ML	Sat Sep 04 22:36:42 2010 +0200
+++ b/src/Pure/Isar/class.ML	Sun Sep 05 19:47:40 2010 +0200
@@ -525,9 +525,8 @@
     val params = map_product get_param tycos class_params |> map_filter I;
     val primary_constraints = map (apsnd
       (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
-    val pp = Syntax.pp_global thy;
     val algebra = Sign.classes_of thy
-      |> fold (fn tyco => Sorts.add_arities pp
+      |> fold (fn tyco => Sorts.add_arities (Syntax.pp_global thy)
             (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
     val consts = Sign.consts_of thy;
     val improve_constraints = AList.lookup (op =)

--- a/src/Pure/Isar/local_defs.ML	Sat Sep 04 22:36:42 2010 +0200
+++ b/src/Pure/Isar/local_defs.ML	Sun Sep 05 19:47:40 2010 +0200
@@ -47,7 +47,7 @@
     fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^
       quote (Syntax.string_of_term ctxt eq));
     val ((lhs, _), eq') = eq
-      |> Sign.no_vars (Syntax.pp ctxt)
+      |> Sign.no_vars ctxt
       |> Primitive_Defs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
       handle TERM (msg, _) => err msg | ERROR msg => err msg;
   in (Term.dest_Free (Term.head_of lhs), eq') end;

--- a/src/Pure/axclass.ML	Sat Sep 04 22:36:42 2010 +0200
+++ b/src/Pure/axclass.ML	Sun Sep 05 19:47:40 2010 +0200
@@ -507,8 +507,7 @@
 
 fun define_class (bclass, raw_super) raw_params raw_specs thy =
   let
-    val ctxt = ProofContext.init_global thy;
-    val pp = Syntax.pp ctxt;
+    val ctxt = Syntax.init_pretty_global thy;
 
 
     (* class *)
@@ -520,8 +519,8 @@
     fun check_constraint (a, S) =
       if Sign.subsort thy (super, S) then ()
       else error ("Sort constraint of type variable " ^
-        setmp_CRITICAL show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^
-        " needs to be weaker than " ^ Pretty.string_of_sort pp super);
+        setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) (TFree (a, S)) ^
+        " needs to be weaker than " ^ Syntax.string_of_sort ctxt super);
 
 
     (* params *)
@@ -543,7 +542,7 @@
       (case Term.add_tfrees t [] of
         [(a, S)] => check_constraint (a, S)
       | [] => ()
-      | _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t);
+      | _ => error ("Multiple type variables in class axiom:\n" ^ Syntax.string_of_term ctxt t);
       t
       |> Term.map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
       |> Logic.close_form);
@@ -590,7 +589,7 @@
       |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> #2
       |> Sign.restore_naming facts_thy
       |> map_axclasses (Symtab.update (class, axclass))
-      |> map_params (fold (fn (x, _) => add_param pp (x, class)) params);
+      |> map_params (fold (fn (x, _) => add_param (Syntax.pp ctxt) (x, class)) params);
 
   in (class, result_thy) end;
 

--- a/src/Pure/more_thm.ML	Sat Sep 04 22:36:42 2010 +0200
+++ b/src/Pure/more_thm.ML	Sun Sep 05 19:47:40 2010 +0200
@@ -348,7 +348,7 @@
   let
     val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
 
-    val _ = Sign.no_vars (Syntax.pp_global thy) prop;
+    val _ = Sign.no_vars (Syntax.init_pretty_global thy) prop;
     val (strip, recover, prop') = stripped_sorts thy prop;
     val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
     val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
@@ -365,7 +365,7 @@
 
 fun add_def unchecked overloaded (b, prop) thy =
   let
-    val _ = Sign.no_vars (Syntax.pp_global thy) prop;
+    val _ = Sign.no_vars (Syntax.init_pretty_global thy) prop;
     val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
     val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
 

--- a/src/Pure/sign.ML	Sat Sep 04 22:36:42 2010 +0200
+++ b/src/Pure/sign.ML	Sun Sep 05 19:47:40 2010 +0200
@@ -67,8 +67,8 @@
   val certify_term: theory -> term -> term * typ * int
   val cert_term: theory -> term -> term
   val cert_prop: theory -> term -> term
-  val no_frees: Pretty.pp -> term -> term
-  val no_vars: Pretty.pp -> term -> term
+  val no_frees: Proof.context -> term -> term
+  val no_vars: Proof.context -> term -> term
   val add_types: (binding * int * mixfix) list -> theory -> theory
   val add_nonterminals: binding list -> theory -> theory
   val add_type_abbrev: binding * string list * typ -> theory -> theory
@@ -320,12 +320,13 @@
 
 (* specifications *)
 
-fun no_variables kind add addT mk mkT pp tm =
+fun no_variables kind add addT mk mkT ctxt tm =
   (case (add tm [], addT tm []) of
     ([], []) => tm
   | (frees, tfrees) => error (Pretty.string_of (Pretty.block
       (Pretty.str ("Illegal " ^ kind ^ " variable(s) in term:") :: Pretty.brk 1 ::
-       Pretty.commas (map (Pretty.term pp o mk) frees @ map (Pretty.typ pp o mkT) tfrees)))));
+       Pretty.commas
+        (map (Syntax.pretty_term ctxt o mk) frees @ map (Syntax.pretty_typ ctxt o mkT) tfrees)))));
 
 val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree;
 val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar;
@@ -434,12 +435,12 @@
 
 fun add_abbrev mode (b, raw_t) thy =
   let
-    val pp = Syntax.pp_global thy;
-    val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
+    val ctxt = Syntax.init_pretty_global thy;
+    val prep_tm = no_frees ctxt o Term.no_dummy_patterns o cert_term_abbrev thy;
     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
     val (res, consts') = consts_of thy
-      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode (b, t);
+      |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of thy) (naming_of thy) mode (b, t);
   in (res, thy |> map_consts (K consts')) end;
 
 fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);

--- a/src/Pure/theory.ML	Sat Sep 04 22:36:42 2010 +0200
+++ b/src/Pure/theory.ML	Sun Sep 05 19:47:40 2010 +0200
@@ -167,7 +167,7 @@
       error ("Illegal sort constraints in primitive specification: " ^
         commas (map (setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy)) bad_sorts));
   in
-    (b, Sign.no_vars (Syntax.pp_global thy) t)
+    (b, Sign.no_vars (Syntax.init_pretty_global thy) t)
   end handle ERROR msg =>
     cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
 
@@ -182,10 +182,10 @@
 
 fun dependencies thy unchecked def description lhs rhs =
   let
-    val pp = Syntax.pp_global thy;
+    val ctxt = Syntax.init_pretty_global thy;
     val consts = Sign.consts_of thy;
     fun prep const =
-      let val Const (c, T) = Sign.no_vars pp (Const const)
+      let val Const (c, T) = Sign.no_vars ctxt (Const const)
       in (c, Consts.typargs consts (c, Logic.varifyT_global T)) end;
 
     val lhs_vars = Term.add_tfreesT (#2 lhs) [];
@@ -194,9 +194,9 @@
     val _ =
       if null rhs_extras then ()
       else error ("Specification depends on extra type variables: " ^
-        commas_quote (map (Pretty.string_of_typ pp o TFree) rhs_extras) ^
+        commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
         "\nThe error(s) above occurred in " ^ quote description);
-  in Defs.define pp unchecked def description (prep lhs) (map prep rhs) end;
+  in Defs.define (Syntax.pp ctxt) unchecked def description (prep lhs) (map prep rhs) end;
 
 fun add_deps a raw_lhs raw_rhs thy =
   let

--- a/src/Tools/Code/code_preproc.ML	Sat Sep 04 22:36:42 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Sun Sep 05 19:47:40 2010 +0200
@@ -429,10 +429,9 @@
 
 fun dynamic_eval thy cterm_of conclude_evaluation evaluator proto_ct =
   let
-    val pp = Syntax.pp_global thy;
+    val ctxt = Syntax.init_pretty_global thy;
     val ct = cterm_of proto_ct;
-    val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp)
-      (Thm.term_of ct);
+    val _ = (Sign.no_frees ctxt o map_types (K dummyT) o Sign.no_vars ctxt) (Thm.term_of ct);
     val thm = preprocess_conv thy ct;
     val ct' = Thm.rhs_of thm;
     val (vs', t') = dest_cterm ct';