src/Pure/Isar/isar_cmd.ML
changeset 56155 1b9c089ed12d
parent 56072 31e427387ab5
child 56158 c2c6d560e7b2
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 15 08:31:33 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Mar 15 10:14:42 2014 +0100
     1.3 @@ -256,7 +256,7 @@
     1.4  (* print theorems *)
     1.5  
     1.6  val print_theorems_proof =
     1.7 -  Toplevel.keep (Proof_Context.print_lthms o Proof.context_of o Toplevel.proof_of);
     1.8 +  Toplevel.keep (Proof_Context.print_local_facts o Proof.context_of o Toplevel.proof_of);
     1.9  
    1.10  fun print_theorems_theory verbose = Toplevel.keep (fn state =>
    1.11    Toplevel.theory_of state |>