src/Pure/Isar/proof_context.ML
changeset 50126 3dec88149176
parent 49888 ff2063be8227
child 50201 c26369c9eda6
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Nov 19 18:01:48 2012 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Nov 19 20:23:47 2012 +0100
     1.3 @@ -52,7 +52,6 @@
     1.4    val extern_fact: Proof.context -> string -> xstring
     1.5    val pretty_term_abbrev: Proof.context -> term -> Pretty.T
     1.6    val markup_fact: Proof.context -> string -> Markup.T
     1.7 -  val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
     1.8    val pretty_fact: Proof.context -> string * thm list -> Pretty.T
     1.9    val read_class: Proof.context -> xstring -> class
    1.10    val read_typ: Proof.context -> string -> typ
    1.11 @@ -343,14 +342,11 @@
    1.12  fun pretty_fact_name ctxt a =
    1.13    Pretty.block [Pretty.mark_str (markup_fact ctxt a, extern_fact ctxt a), Pretty.str ":"];
    1.14  
    1.15 -fun pretty_fact_aux ctxt flag ("", ths) =
    1.16 -      Display.pretty_thms_aux ctxt flag ths
    1.17 -  | pretty_fact_aux ctxt flag (a, [th]) = Pretty.block
    1.18 -      [pretty_fact_name ctxt a, Pretty.brk 1, Display.pretty_thm_aux ctxt flag th]
    1.19 -  | pretty_fact_aux ctxt flag (a, ths) = Pretty.block
    1.20 -      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (Display.pretty_thm_aux ctxt flag) ths));
    1.21 -
    1.22 -fun pretty_fact ctxt = pretty_fact_aux ctxt true;
    1.23 +fun pretty_fact ctxt ("", ths) = Display.pretty_thms ctxt ths
    1.24 +  | pretty_fact ctxt (a, [th]) = Pretty.block
    1.25 +      [pretty_fact_name ctxt a, Pretty.brk 1, Display.pretty_thm ctxt th]
    1.26 +  | pretty_fact ctxt (a, ths) = Pretty.block
    1.27 +      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (Display.pretty_thm ctxt) ths));
    1.28  
    1.29  
    1.30