clarified pretty_goals, pretty_thm_aux: plain context;
explicit pretty_goals_without_context, print_goals_without_context;
tuned;

--- a/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jul 23 16:43:31 2009 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jul 23 16:52:16 2009 +0200
@@ -140,7 +140,7 @@
 fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table))
 
 fun pr_goals ctxt st =
-    Display_Goal.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st
+    Display_Goal.pretty_goals ctxt Markup.none (true, false) (Thm.nprems_of st) st
      |> Pretty.chunks
      |> Pretty.string_of
 

--- a/src/Pure/Isar/proof.ML	Thu Jul 23 16:43:31 2009 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Jul 23 16:52:16 2009 +0200
@@ -318,8 +318,6 @@
 val show_main_goal = ref false;
 val verbose = ProofContext.verbose;
 
-val pretty_goals_local = Display_Goal.pretty_goals_aux o Syntax.pp;
-
 fun pretty_facts _ _ NONE = []
   | pretty_facts s ctxt (SOME ths) =
       [Pretty.big_list (s ^ "this:") (map (Display.pretty_thm ctxt) ths), Pretty.str ""];
@@ -346,7 +344,7 @@
             (if mode <> Backward orelse null using then NONE else SOME using) @
           [Pretty.str ("goal" ^
             description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
-          pretty_goals_local ctxt Markup.subgoal
+          Display_Goal.pretty_goals ctxt Markup.subgoal
             (true, ! show_main_goal) (! Display.goals_limit) goal @
           (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
       | prt_goal NONE = [];
@@ -368,7 +366,7 @@
 
 fun pretty_goals main state =
   let val (ctxt, (_, goal)) = get_goal state
-  in pretty_goals_local ctxt Markup.none (false, main) (! Display.goals_limit) goal end;
+  in Display_Goal.pretty_goals ctxt Markup.none (false, main) (! Display.goals_limit) goal end;
 
 
 
@@ -474,7 +472,8 @@
 
     val ngoals = Thm.nprems_of goal;
     val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
-      (pretty_goals_local ctxt Markup.none (true, ! show_main_goal) (! Display.goals_limit) goal @
+      (Display_Goal.pretty_goals ctxt Markup.none
+          (true, ! show_main_goal) (! Display.goals_limit) goal @
         [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])));
 
     val extra_hyps = Assumption.extra_hyps ctxt goal;

--- a/src/Pure/Isar/proof_display.ML	Thu Jul 23 16:43:31 2009 +0200
+++ b/src/Pure/Isar/proof_display.ML	Thu Jul 23 16:52:16 2009 +0200
@@ -35,7 +35,7 @@
   let
     val thy = Thm.theory_of_thm th;
     val flags = {quote = true, show_hyps = false, show_status = true};
-  in Display.pretty_thm_raw (Syntax.pp_global thy) flags [] th end;
+  in Display.pretty_thm_raw (Syntax.init_pretty_global thy) flags th end;
 
 val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
 val pp_term = Pretty.quote oo Syntax.pretty_term_global;

--- a/src/Pure/Proof/reconstruct.ML	Thu Jul 23 16:43:31 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Thu Jul 23 16:52:16 2009 +0200
@@ -255,7 +255,7 @@
       let
         fun search env [] = error ("Unsolvable constraints:\n" ^
               Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
-                Display_Goal.pretty_flexpair (Syntax.pp_global thy) (pairself
+                Display_Goal.pretty_flexpair (Syntax.init_pretty_global thy) (pairself
                   (Envir.norm_term bigenv) p)) cs)))
           | search env ((u, p as (t1, t2), vs)::ps) =
               if u then

--- a/src/Pure/display.ML	Thu Jul 23 16:43:31 2009 +0200
+++ b/src/Pure/display.ML	Thu Jul 23 16:52:16 2009 +0200
@@ -16,8 +16,8 @@
 signature DISPLAY =
 sig
   include BASIC_DISPLAY
-  val pretty_thm_raw: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
-    term list -> thm -> Pretty.T
+  val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool, show_status: bool} ->
+    thm -> Pretty.T
   val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
   val pretty_thm_global: theory -> thm -> Pretty.T
@@ -68,7 +68,7 @@
         else ""
       end;
 
-fun pretty_thm_raw pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
+fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps', show_status} raw_th =
   let
     val th = Thm.strip_shyps raw_th;
     val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
@@ -76,8 +76,9 @@
     val tags = Thm.get_tags th;
 
     val q = if quote then Pretty.quote else I;
-    val prt_term = q o Pretty.term pp;
+    val prt_term = q o Syntax.pretty_term ctxt;
 
+    val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
     val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
     val status = display_status show_status th;
 
@@ -86,8 +87,8 @@
       if hlen = 0 andalso status = "" then []
       else if ! show_hyps orelse show_hyps' then
         [Pretty.brk 2, Pretty.list "[" "]"
-          (map (q o Display_Goal.pretty_flexpair pp) tpairs @ map prt_term hyps' @
-           map (Pretty.sort pp) xshyps @
+          (map (q o Display_Goal.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
+           map (Syntax.pretty_sort ctxt) xshyps @
             (if status = "" then [] else [Pretty.str status]))]
       else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
     val tsymbs =
@@ -95,18 +96,14 @@
       else [Pretty.brk 1, pretty_tags tags];
   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
 
-fun pretty_thm_aux ctxt show_status th =
-  let
-    val flags = {quote = false, show_hyps = true, show_status = show_status};
-    val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
-  in pretty_thm_raw (Syntax.pp ctxt) flags asms th end;
-
+fun pretty_thm_aux ctxt show_status =
+  pretty_thm_raw ctxt {quote = false, show_hyps = true, show_status = show_status};
 
 fun pretty_thm ctxt = pretty_thm_aux ctxt true;
 
-fun pretty_thm_global thy th =
-  pretty_thm_raw (Syntax.pp_global thy)
-    {quote = false, show_hyps = false, show_status = true} [] th;
+fun pretty_thm_global thy =
+  pretty_thm_raw (Syntax.init_pretty_global thy)
+    {quote = false, show_hyps = false, show_status = true};
 
 fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th;
 

--- a/src/Pure/display_goal.ML	Thu Jul 23 16:43:31 2009 +0200
+++ b/src/Pure/display_goal.ML	Thu Jul 23 16:52:16 2009 +0200
@@ -9,10 +9,10 @@
 sig
   val goals_limit: int ref
   val show_consts: bool ref
-  val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
-  val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
-  val pretty_goals: int -> thm -> Pretty.T list
-  val print_goals: int -> thm -> unit
+  val pretty_flexpair: Proof.context -> term * term -> Pretty.T
+  val pretty_goals: Proof.context -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
+  val pretty_goals_without_context: int -> thm -> Pretty.T list
+  val print_goals_without_context: int -> thm -> unit
 end;
 
 structure Display_Goal: DISPLAY_GOAL =
@@ -21,8 +21,8 @@
 val goals_limit = ref 10;      (*max number of goals to print*)
 val show_consts = ref false;   (*true: show consts with types in proof state output*)
 
-fun pretty_flexpair pp (t, u) = Pretty.block
-  [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
+fun pretty_flexpair ctxt (t, u) = Pretty.block
+  [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
 
 
 (*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
@@ -56,31 +56,35 @@
 
 in
 
-fun pretty_goals_aux pp markup (msg, main) maxgoals state =
+fun pretty_goals ctxt markup (msg, main) maxgoals state =
   let
+    val prt_sort = Syntax.pretty_sort ctxt;
+    val prt_typ = Syntax.pretty_typ ctxt;
+    val prt_term = Syntax.pretty_term ctxt;
+
     fun prt_atoms prt prtT (X, xs) = Pretty.block
       [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
         Pretty.brk 1, prtT X];
 
-    fun prt_var (x, ~1) = Pretty.term pp (Syntax.free x)
-      | prt_var xi = Pretty.term pp (Syntax.var xi);
+    fun prt_var (x, ~1) = prt_term (Syntax.free x)
+      | prt_var xi = prt_term (Syntax.var xi);
 
-    fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, []))
-      | prt_varT xi = Pretty.typ pp (TVar (xi, []));
+    fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
+      | prt_varT xi = prt_typ (TVar (xi, []));
 
-    val prt_consts = prt_atoms (Pretty.term pp o Const) (Pretty.typ pp);
-    val prt_vars = prt_atoms prt_var (Pretty.typ pp);
-    val prt_varsT = prt_atoms prt_varT (Pretty.sort pp);
+    val prt_consts = prt_atoms (prt_term o Const) prt_typ;
+    val prt_vars = prt_atoms prt_var prt_typ;
+    val prt_varsT = prt_atoms prt_varT prt_sort;
 
 
     fun pretty_list _ _ [] = []
       | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
 
     fun pretty_subgoal (n, A) = Pretty.markup markup
-      [Pretty.str (" " ^ string_of_int n ^ ". "), Pretty.term pp A];
+      [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
     fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
 
-    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp);
+    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
 
     val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
     val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
@@ -92,7 +96,7 @@
     val ngoals = length As;
 
     fun pretty_gs (types, sorts) =
-      (if main then [Pretty.term pp B] else []) @
+      (if main then [prt_term B] else []) @
        (if ngoals = 0 then [Pretty.str "No subgoals!"]
         else if ngoals > maxgoals then
           pretty_subgoals (Library.take (maxgoals, As)) @
@@ -110,10 +114,11 @@
    (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
   end;
 
-fun pretty_goals n th =
-  pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
+fun pretty_goals_without_context n th =
+  pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
 
-val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
+val print_goals_without_context =
+  (Pretty.writeln o Pretty.chunks) oo pretty_goals_without_context;
 
 end;
 

--- a/src/Pure/goal.ML	Thu Jul 23 16:43:31 2009 +0200
+++ b/src/Pure/goal.ML	Thu Jul 23 16:52:16 2009 +0200
@@ -78,7 +78,7 @@
   (case Thm.nprems_of th of
     0 => conclude th
   | n => raise THM ("Proof failed.\n" ^
-      Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals n th)) ^
+      Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals_without_context n th)) ^
       ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
 
 

--- a/src/Pure/old_goals.ML	Thu Jul 23 16:43:31 2009 +0200
+++ b/src/Pure/old_goals.ML	Thu Jul 23 16:52:16 2009 +0200
@@ -135,7 +135,8 @@
 (*Default action is to print an error message; could be suppressed for
   special applications.*)
 fun result_error_default state msg : thm =
-  Pretty.str "Bad final proof state:" :: Display_Goal.pretty_goals (!goals_limit) state @
+  Pretty.str "Bad final proof state:" ::
+      Display_Goal.pretty_goals_without_context (!goals_limit) state @
     [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
 
 val result_error_fn = ref result_error_default;
@@ -277,7 +278,7 @@
       (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
         (if ngoals <> 1 then "s" else "") ^ ")"
       else ""))] @
-    Display_Goal.pretty_goals m th
+    Display_Goal.pretty_goals_without_context m th
   end |> Pretty.chunks |> Pretty.writeln;
 
 (*Printing can raise exceptions, so the assignment occurs last.

--- a/src/Pure/tctical.ML	Thu Jul 23 16:43:31 2009 +0200
+++ b/src/Pure/tctical.ML	Thu Jul 23 16:52:16 2009 +0200
@@ -191,12 +191,11 @@
 (*** Tracing tactics ***)
 
 (*Print the current proof state and pass it on.*)
-fun print_tac msg =
-    (fn st =>
-     (tracing msg;
-      tracing ((Pretty.string_of o Pretty.chunks o
-                 Display_Goal.pretty_goals (! Display_Goal.goals_limit)) st);
-      Seq.single st));
+fun print_tac msg st =
+ (tracing (msg ^ "\n" ^
+    Pretty.string_of (Pretty.chunks
+      (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st)));
+  Seq.single st);
 
 (*Pause until a line is typed -- if non-empty then fail. *)
 fun pause_tac st =
@@ -232,10 +231,10 @@
 
 (*Extract from a tactic, a thm->thm seq function that handles tracing*)
 fun tracify flag tac st =
-  if !flag andalso not (!suppress_tracing)
-           then (Display_Goal.print_goals (! Display_Goal.goals_limit) st;
-                 tracing "** Press RETURN to continue:";
-                 exec_trace_command flag (tac,st))
+  if !flag andalso not (!suppress_tracing) then
+   (Display_Goal.print_goals_without_context (! Display_Goal.goals_limit) st;
+    tracing "** Press RETURN to continue:";
+    exec_trace_command flag (tac, st))
   else tac st;
 
 (*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)