--- a/src/Pure/Isar/isar_syn.ML Fri Jun 27 15:41:26 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML Fri Jun 27 16:04:56 2014 +0200
@@ -897,9 +897,18 @@
(Parse_Spec.xthms1 >> Isar_Cmd.thm_deps);
val _ =
- Outer_Syntax.improper_command @{command_spec "print_binds"} "print term bindings of proof context"
+ Outer_Syntax.improper_command @{command_spec "print_binds"}
+ "print term bindings of proof context -- Proof General legacy"
(Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_binds o Toplevel.context_of)));
+ Toplevel.keep
+ (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
+
+val _ =
+ Outer_Syntax.improper_command @{command_spec "print_term_bindings"}
+ "print term bindings of proof context"
+ (Scan.succeed (Toplevel.unknown_context o
+ Toplevel.keep
+ (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
val _ =
Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"