src/Pure/Isar/proof_display.ML
changeset 20311 3666316adad6
parent 20253 636ac45d100f
child 20621 29d57880ba00
     1.1 --- a/src/Pure/Isar/proof_display.ML	Wed Aug 02 22:27:04 2006 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Wed Aug 02 22:27:05 2006 +0200
     1.3 @@ -14,18 +14,17 @@
     1.4  signature PROOF_DISPLAY =
     1.5  sig
     1.6    include BASIC_PROOF_DISPLAY
     1.7 -  val debug: bool ref
     1.8 -  val pprint_context: ProofContext.context -> pprint_args -> unit
     1.9 +  val pprint_context: Proof.context -> pprint_args -> unit
    1.10    val pprint_typ: theory -> typ -> pprint_args -> unit
    1.11    val pprint_term: theory -> term -> pprint_args -> unit
    1.12    val pprint_ctyp: ctyp -> pprint_args -> unit
    1.13    val pprint_cterm: cterm -> pprint_args -> unit
    1.14    val pprint_thm: thm -> pprint_args -> unit
    1.15    val print_theorems_diff: theory -> theory -> unit
    1.16 -  val string_of_rule: ProofContext.context -> string -> thm -> string
    1.17 -  val print_results: bool -> ProofContext.context ->
    1.18 +  val string_of_rule: Proof.context -> string -> thm -> string
    1.19 +  val print_results: bool -> Proof.context ->
    1.20      ((string * string) * (string * thm list) list) -> unit
    1.21 -  val present_results: ProofContext.context ->
    1.22 +  val present_results: Proof.context ->
    1.23      ((string * string) * (string * thm list) list) -> unit
    1.24  end
    1.25  
    1.26 @@ -34,10 +33,8 @@
    1.27  
    1.28  (* toplevel pretty printing *)
    1.29  
    1.30 -val debug = ref false;
    1.31 -
    1.32  fun pprint_context ctxt = Pretty.pprint
    1.33 - (if ! debug then
    1.34 + (if ! ProofContext.debug then
    1.35      Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
    1.36    else Pretty.str "<context>");
    1.37