moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
load display.ML after assumption.ML, to accomodate proper contextual theorem display;

--- a/src/HOL/Tools/Function/lexicographic_order.ML	Mon Jul 20 20:03:19 2009 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Mon Jul 20 21:20:09 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.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st
+    Display_Goal.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st
      |> Pretty.chunks
      |> Pretty.string_of
 

--- a/src/Pure/IsaMakefile	Mon Jul 20 20:03:19 2009 +0200
+++ b/src/Pure/IsaMakefile	Mon Jul 20 21:20:09 2009 +0200
@@ -90,13 +90,13 @@
   Tools/find_theorems.ML Tools/named_thms.ML Tools/xml_syntax.ML	\
   assumption.ML axclass.ML codegen.ML config.ML conjunction.ML		\
   consts.ML context.ML context_position.ML conv.ML defs.ML display.ML	\
-  drule.ML envir.ML facts.ML goal.ML interpretation.ML item_net.ML	\
-  library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML	\
-  name.ML net.ML old_goals.ML old_term.ML pattern.ML primitive_defs.ML	\
-  proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML		\
-  simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML	\
-  term_ord.ML term_subst.ML theory.ML thm.ML type.ML type_infer.ML	\
-  unify.ML variable.ML
+  display_goal.ML drule.ML envir.ML facts.ML goal.ML interpretation.ML	\
+  item_net.ML library.ML logic.ML meta_simplifier.ML more_thm.ML	\
+  morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML	\
+  primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML	\
+  sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML	\
+  term.ML term_ord.ML term_subst.ML theory.ML thm.ML type.ML		\
+  type_infer.ML unify.ML variable.ML
 	@./mk
 
 

--- a/src/Pure/Isar/proof.ML	Mon Jul 20 20:03:19 2009 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Jul 20 21:20:09 2009 +0200
@@ -318,7 +318,7 @@
 val show_main_goal = ref false;
 val verbose = ProofContext.verbose;
 
-val pretty_goals_local = Display.pretty_goals_aux o Syntax.pp;
+val pretty_goals_local = Display_Goal.pretty_goals_aux o Syntax.pp;
 
 fun pretty_facts _ _ NONE = []
   | pretty_facts s ctxt (SOME ths) =

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

--- a/src/Pure/ROOT.ML	Mon Jul 20 20:03:19 2009 +0200
+++ b/src/Pure/ROOT.ML	Mon Jul 20 21:20:09 2009 +0200
@@ -115,17 +115,18 @@
 use "more_thm.ML";
 use "facts.ML";
 use "pure_thy.ML";
-use "display.ML";
 use "drule.ML";
 use "morphism.ML";
 use "variable.ML";
 use "conv.ML";
+use "display_goal.ML";
 use "tctical.ML";
 use "search.ML";
 use "tactic.ML";
 use "meta_simplifier.ML";
 use "conjunction.ML";
 use "assumption.ML";
+use "display.ML";
 use "goal.ML";
 use "axclass.ML";
 

--- a/src/Pure/display.ML	Mon Jul 20 20:03:19 2009 +0200
+++ b/src/Pure/display.ML	Mon Jul 20 21:20:09 2009 +0200
@@ -1,22 +1,21 @@
 (*  Title:      Pure/display.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+    Author:     Makarius
 
-Printing of theorems, goals, results etc.
+Printing of theorems, results etc.
 *)
 
 signature BASIC_DISPLAY =
 sig
   val goals_limit: int ref
+  val show_consts: bool ref
   val show_hyps: bool ref
   val show_tags: bool ref
-  val show_consts: bool ref
 end;
 
 signature DISPLAY =
 sig
   include BASIC_DISPLAY
-  val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
   val pretty_thm_aux: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
     term list -> thm -> Pretty.T
   val pretty_thm: thm -> Pretty.T
@@ -37,27 +36,26 @@
   val print_cterm: cterm -> unit
   val print_syntax: theory -> unit
   val pretty_full_theory: bool -> theory -> Pretty.T list
-  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
 end;
 
 structure Display: DISPLAY =
 struct
 
+(** options **)
+
+val goals_limit = Display_Goal.goals_limit;
+val show_consts = Display_Goal.show_consts;
+
+val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
+val show_tags = ref false;      (*false: suppress tags*)
+
+
 
 (** print thm **)
 
-val goals_limit = ref 10;       (*max number of goals to print*)
-val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
-val show_tags = ref false;      (*false: suppress tags*)
-
 fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
 
-fun pretty_flexpair pp (t, u) = Pretty.block
-  [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
-
 fun display_status false _ = ""
   | display_status true th =
       let
@@ -89,7 +87,7 @@
       if hlen = 0 andalso status = "" then []
       else if ! show_hyps orelse show_hyps' then
         [Pretty.brk 2, Pretty.list "[" "]"
-          (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @
+          (map (q o Display_Goal.pretty_flexpair pp) tpairs @ map prt_term hyps' @
            map (Pretty.sort pp) xshyps @
             (if status = "" then [] else [Pretty.str status]))]
       else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
@@ -242,109 +240,7 @@
          Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]]
   end;
 
-
-
-(** print_goals **)
-
-(* print_goals etc. *)
-
-val show_consts = ref false;  (*true: show consts with types in proof state output*)
-
-
-(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
-
-local
-
-fun ins_entry (x, y) =
-  AList.default (op =) (x, []) #>
-  AList.map_entry (op =) x (insert (op =) y);
-
-val add_consts = Term.fold_aterms
-  (fn Const (c, T) => ins_entry (T, (c, T))
-    | _ => I);
-
-val add_vars = Term.fold_aterms
-  (fn Free (x, T) => ins_entry (T, (x, ~1))
-    | Var (xi, T) => ins_entry (T, xi)
-    | _ => I);
-
-val add_varsT = Term.fold_atyps
-  (fn TFree (x, S) => ins_entry (S, (x, ~1))
-    | TVar (xi, S) => ins_entry (S, xi)
-    | _ => I);
-
-fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
-fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
-
-fun consts_of t = sort_cnsts (add_consts t []);
-fun vars_of t = sort_idxs (add_vars t []);
-fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
-
-in
-
-fun pretty_goals_aux pp markup (msg, main) maxgoals state =
-  let
-    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_varT (x, ~1) = Pretty.typ pp (TFree (x, []))
-      | prt_varT xi = Pretty.typ pp (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);
-
-
-    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];
-    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_consts = pretty_list "constants:" prt_consts o consts_of;
-    val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
-    val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
-
-
-    val {prop, tpairs, ...} = Thm.rep_thm state;
-    val (As, B) = Logic.strip_horn prop;
-    val ngoals = length As;
-
-    fun pretty_gs (types, sorts) =
-      (if main then [Pretty.term pp B] else []) @
-       (if ngoals = 0 then [Pretty.str "No subgoals!"]
-        else if ngoals > maxgoals then
-          pretty_subgoals (Library.take (maxgoals, As)) @
-          (if msg then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
-           else [])
-        else pretty_subgoals As) @
-      pretty_ffpairs tpairs @
-      (if ! show_consts then pretty_consts prop else []) @
-      (if types then pretty_vars prop else []) @
-      (if sorts then pretty_varsT prop else []);
-  in
-    setmp show_no_free_types true
-      (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
-        (setmp show_sorts false pretty_gs))
-   (! 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;
-
-val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
-
 end;
 
-
-end;
-
-structure BasicDisplay: BASIC_DISPLAY = Display;
-open BasicDisplay;
+structure Basic_Display: BASIC_DISPLAY = Display;
+open Basic_Display;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/display_goal.ML	Mon Jul 20 21:20:09 2009 +0200
@@ -0,0 +1,121 @@
+(*  Title:      Pure/display_goal.ML
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Makarius
+
+Display tactical goal state.
+*)
+
+signature DISPLAY_GOAL =
+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
+end;
+
+structure Display_Goal: DISPLAY_GOAL =
+struct
+
+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];
+
+
+(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
+
+local
+
+fun ins_entry (x, y) =
+  AList.default (op =) (x, []) #>
+  AList.map_entry (op =) x (insert (op =) y);
+
+val add_consts = Term.fold_aterms
+  (fn Const (c, T) => ins_entry (T, (c, T))
+    | _ => I);
+
+val add_vars = Term.fold_aterms
+  (fn Free (x, T) => ins_entry (T, (x, ~1))
+    | Var (xi, T) => ins_entry (T, xi)
+    | _ => I);
+
+val add_varsT = Term.fold_atyps
+  (fn TFree (x, S) => ins_entry (S, (x, ~1))
+    | TVar (xi, S) => ins_entry (S, xi)
+    | _ => I);
+
+fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
+fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
+
+fun consts_of t = sort_cnsts (add_consts t []);
+fun vars_of t = sort_idxs (add_vars t []);
+fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
+
+in
+
+fun pretty_goals_aux pp markup (msg, main) maxgoals state =
+  let
+    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_varT (x, ~1) = Pretty.typ pp (TFree (x, []))
+      | prt_varT xi = Pretty.typ pp (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);
+
+
+    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];
+    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_consts = pretty_list "constants:" prt_consts o consts_of;
+    val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
+    val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
+
+
+    val {prop, tpairs, ...} = Thm.rep_thm state;
+    val (As, B) = Logic.strip_horn prop;
+    val ngoals = length As;
+
+    fun pretty_gs (types, sorts) =
+      (if main then [Pretty.term pp B] else []) @
+       (if ngoals = 0 then [Pretty.str "No subgoals!"]
+        else if ngoals > maxgoals then
+          pretty_subgoals (Library.take (maxgoals, As)) @
+          (if msg then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
+           else [])
+        else pretty_subgoals As) @
+      pretty_ffpairs tpairs @
+      (if ! show_consts then pretty_consts prop else []) @
+      (if types then pretty_vars prop else []) @
+      (if sorts then pretty_varsT prop else []);
+  in
+    setmp show_no_free_types true
+      (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
+        (setmp show_sorts false pretty_gs))
+   (! 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;
+
+val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
+
+end;
+
+end;
+

--- a/src/Pure/goal.ML	Mon Jul 20 20:03:19 2009 +0200
+++ b/src/Pure/goal.ML	Mon Jul 20 21:20:09 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.pretty_goals n th)) ^
+      Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals n th)) ^
       ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
 
 

--- a/src/Pure/old_goals.ML	Mon Jul 20 20:03:19 2009 +0200
+++ b/src/Pure/old_goals.ML	Mon Jul 20 21:20:09 2009 +0200
@@ -135,7 +135,7 @@
 (*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.pretty_goals (!goals_limit) state @
+  Pretty.str "Bad final proof state:" :: Display_Goal.pretty_goals (!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 +277,7 @@
       (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
         (if ngoals <> 1 then "s" else "") ^ ")"
       else ""))] @
-    Display.pretty_goals m th
+    Display_Goal.pretty_goals m th
   end |> Pretty.chunks |> Pretty.writeln;
 
 (*Printing can raise exceptions, so the assignment occurs last.

--- a/src/Pure/tctical.ML	Mon Jul 20 20:03:19 2009 +0200
+++ b/src/Pure/tctical.ML	Mon Jul 20 21:20:09 2009 +0200
@@ -195,7 +195,7 @@
     (fn st =>
      (tracing msg;
       tracing ((Pretty.string_of o Pretty.chunks o
-                 Display.pretty_goals (! Display.goals_limit)) st);
+                 Display_Goal.pretty_goals (! Display_Goal.goals_limit)) st);
       Seq.single st));
 
 (*Pause until a line is typed -- if non-empty then fail. *)
@@ -233,7 +233,7 @@
 (*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.print_goals (! Display.goals_limit) st;
+           then (Display_Goal.print_goals (! Display_Goal.goals_limit) st;
                  tracing "** Press RETURN to continue:";
                  exec_trace_command flag (tac,st))
   else tac st;