1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 26 14:14:02 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 26 15:18:50 2009 +0100
     1.3 @@ -36,6 +36,9 @@
     1.4    val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
     1.5    val extern_fact: Proof.context -> string -> xstring
     1.6    val pretty_term_abbrev: Proof.context -> term -> Pretty.T
     1.7 +  val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
     1.8 +  val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
     1.9 +  val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
    1.10    val pretty_thm: Proof.context -> thm -> Pretty.T
    1.11    val pretty_thms: Proof.context -> thm list -> Pretty.T
    1.12    val pretty_fact: Proof.context -> string * thm list -> Pretty.T
    1.13 @@ -295,21 +298,28 @@
    1.14  
    1.15  fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
    1.16  
    1.17 -fun pretty_thm ctxt th =
    1.18 -  let val asms = map Thm.term_of (Assumption.all_assms_of ctxt)
    1.19 -  in Display.pretty_thm_aux (Syntax.pp ctxt) false true asms th end;
    1.20 +fun pretty_thm_aux ctxt show_status th =
    1.21 +  let
    1.22 +    val flags = {quote = false, show_hyps = true, show_status = show_status};
    1.23 +    val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
    1.24 +  in Display.pretty_thm_aux (Syntax.pp ctxt) flags asms th end;
    1.25  
    1.26 -fun pretty_thms ctxt [th] = pretty_thm ctxt th
    1.27 -  | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
    1.28 +fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th
    1.29 +  | pretty_thms_aux ctxt flag ths =
    1.30 +      Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths));
    1.31  
    1.32  fun pretty_fact_name ctxt a = Pretty.block
    1.33    [Pretty.markup (Markup.fact a) [Pretty.str (extern_fact ctxt a)], Pretty.str ":"];
    1.34  
    1.35 -fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths
    1.36 -  | pretty_fact ctxt (a, [th]) = Pretty.block
    1.37 -      [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm ctxt th]
    1.38 -  | pretty_fact ctxt (a, ths) = Pretty.block
    1.39 -      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (pretty_thm ctxt) ths));
    1.40 +fun pretty_fact_aux ctxt flag ("", ths) = pretty_thms_aux ctxt flag ths
    1.41 +  | pretty_fact_aux ctxt flag (a, [th]) = Pretty.block
    1.42 +      [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm_aux ctxt flag th]
    1.43 +  | pretty_fact_aux ctxt flag (a, ths) = Pretty.block
    1.44 +      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (pretty_thm_aux ctxt flag) ths));
    1.45 +
    1.46 +fun pretty_thm ctxt = pretty_thm_aux ctxt true;
    1.47 +fun pretty_thms ctxt = pretty_thms_aux ctxt true;
    1.48 +fun pretty_fact ctxt = pretty_fact_aux ctxt true;
    1.49  
    1.50  val string_of_thm = Pretty.string_of oo pretty_thm;
    1.51