src/Pure/Isar/proof_context.ML
changeset 6985 2af6405a6ef3
parent 6931 bd8aa6ae6bcd
child 6996 1a28d968c5aa
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Jul 12 22:28:56 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Jul 12 22:29:17 1999 +0200
     1.3 @@ -11,6 +11,8 @@
     1.4    exception CONTEXT of string * context
     1.5    val theory_of: context -> theory
     1.6    val sign_of: context -> Sign.sg
     1.7 +  val show_hyps: bool ref
     1.8 +  val pretty_thm: thm -> Pretty.T
     1.9    val verbose: bool ref
    1.10    val print_binds: context -> unit
    1.11    val print_thms: context -> unit
    1.12 @@ -108,6 +110,9 @@
    1.13  
    1.14  (** print context information **)
    1.15  
    1.16 +val show_hyps = ref false;
    1.17 +fun pretty_thm th = setmp Display.show_hyps (! show_hyps) Display.pretty_thm th;
    1.18 +
    1.19  val verbose = ref false;
    1.20  fun verb f x = if ! verbose then f x else [];
    1.21  val verb_string = verb (Library.single o Pretty.string_of);
    1.22 @@ -145,7 +150,7 @@
    1.23  (* local theorems *)
    1.24  
    1.25  fun strings_of_thms (Context {thms, ...}) =
    1.26 -  strings_of_items Display.pretty_thm_no_hyps "Local theorems:" (Symtab.dest thms);
    1.27 +  strings_of_items pretty_thm "Local theorems:" (Symtab.dest thms);
    1.28  
    1.29  val print_thms = seq writeln o strings_of_thms;
    1.30