src/Pure/Isar/proof_display.ML
changeset 22872 d7189dc8939c
parent 22335 6c4204df6863
child 24920 2a45e400fdad
     1.1 --- a/src/Pure/Isar/proof_display.ML	Tue May 08 17:40:18 2007 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Tue May 08 17:40:20 2007 +0200
     1.3 @@ -21,14 +21,14 @@
     1.4    val pprint_cterm: cterm -> pprint_args -> unit
     1.5    val pprint_thm: thm -> pprint_args -> unit
     1.6    val print_theorems_diff: theory -> theory -> unit
     1.7 -  val print_full_theory: bool -> theory -> unit
     1.8    val pretty_full_theory: bool -> theory -> Pretty.T
     1.9    val string_of_rule: Proof.context -> string -> thm -> string
    1.10    val print_results: bool -> Proof.context ->
    1.11      ((string * string) * (string * thm list) list) -> unit
    1.12    val present_results: Proof.context ->
    1.13      ((string * string) * (string * thm list) list) -> unit
    1.14 -  val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
    1.15 +  val pretty_consts: Proof.context ->
    1.16 +    (string * typ -> bool) -> (string * typ) list -> Pretty.T
    1.17  end
    1.18  
    1.19  structure ProofDisplay: PROOF_DISPLAY =
    1.20 @@ -47,7 +47,7 @@
    1.21  val pprint_term = pprint ProofContext.pretty_term;
    1.22  fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    1.23  fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    1.24 -val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy true;
    1.25 +val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
    1.26  
    1.27  
    1.28  (* theorems and theory *)
    1.29 @@ -68,13 +68,10 @@
    1.30  
    1.31  val print_theorems = Pretty.writeln o pretty_theorems;
    1.32  
    1.33 -fun print_full_theory verbose thy =
    1.34 -  Pretty.writeln (Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]));
    1.35 +fun pretty_full_theory verbose thy =
    1.36 +  Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
    1.37  
    1.38 -val print_theory = print_full_theory false;
    1.39 -
    1.40 -fun pretty_full_theory verbose thy =
    1.41 -    Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
    1.42 +val print_theory = Pretty.writeln o pretty_full_theory false;
    1.43  
    1.44  
    1.45  (* refinement rule *)