src/Pure/Isar/isar_cmd.ML
changeset 56158 c2c6d560e7b2
parent 56155 1b9c089ed12d
child 56204 f70e69208a8c
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 15 10:29:42 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Mar 15 11:22:25 2014 +0100
     1.3 @@ -255,8 +255,9 @@
     1.4  
     1.5  (* print theorems *)
     1.6  
     1.7 -val print_theorems_proof =
     1.8 -  Toplevel.keep (Proof_Context.print_local_facts o Proof.context_of o Toplevel.proof_of);
     1.9 +fun print_theorems_proof verbose =
    1.10 +  Toplevel.keep (fn st =>
    1.11 +    Proof_Context.print_local_facts (Proof.context_of (Toplevel.proof_of st)) verbose);
    1.12  
    1.13  fun print_theorems_theory verbose = Toplevel.keep (fn state =>
    1.14    Toplevel.theory_of state |>
    1.15 @@ -265,7 +266,7 @@
    1.16    | NONE => Proof_Display.print_theorems verbose));
    1.17  
    1.18  fun print_theorems verbose =
    1.19 -  Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof;
    1.20 +  Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof verbose;
    1.21  
    1.22  
    1.23  (* display dependencies *)