diff -r fe1be2844fda -r e721124f1b1e src/Pure/Isar/isar_syn.ML
--- 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"