src/Pure/Isar/proof_display.ML
changeset 44192 a32ca9165928
parent 42717 0bbb56867091
child 44240 4b1a63678839
     1.1 --- a/src/Pure/Isar/proof_display.ML	Sat Aug 13 21:28:01 2011 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Sat Aug 13 22:04:07 2011 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    val print_theory: theory -> unit
     1.5    val string_of_rule: Proof.context -> string -> thm -> string
     1.6    val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
     1.7 -  val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
     1.8 +  val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
     1.9  end
    1.10  
    1.11  structure Proof_Display: PROOF_DISPLAY =
    1.12 @@ -115,13 +115,17 @@
    1.13  
    1.14  fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
    1.15  
    1.16 -in
    1.17 -
    1.18  fun pretty_consts ctxt pred cs =
    1.19    (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
    1.20      [] => pretty_vars ctxt "constants" cs
    1.21    | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
    1.22  
    1.23 +in
    1.24 +
    1.25 +fun print_consts do_print ctxt pred cs =
    1.26 +  if not do_print orelse null cs then ()
    1.27 +  else Pretty.writeln (pretty_consts ctxt pred cs);
    1.28 +
    1.29  end;
    1.30  
    1.31  end;