--- a/src/Pure/Isar/isar_syn.ML Sat Mar 15 08:31:33 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Mar 15 10:14:42 2014 +0100
@@ -877,7 +877,7 @@
val _ =
Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
(Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep (Proof_Context.print_lthms o Toplevel.context_of)));
+ Toplevel.keep (Proof_Context.print_local_facts o Toplevel.context_of)));
val _ =
Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"