diff -r 710cdb9e0d17 -r 12585dfb86fe src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Jan 06 21:06:17 2011 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jan 06 21:06:18 2011 +0100
@@ -836,10 +836,16 @@
 
 val _ =
   Outer_Syntax.improper_command "print_interps"
-    "print interpretations of locale for this theory" Keyword.diag
+    "print interpretations of locale for this theory or proof context" Keyword.diag
     (Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
 
 val _ =
+  Outer_Syntax.improper_command "print_dependencies"
+    "print dependencies of locale expression" Keyword.diag
+    (opt_bang -- Parse_Spec.locale_expression true >>
+      (Toplevel.no_timing oo Isar_Cmd.print_dependencies));
+
+val _ =
   Outer_Syntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_attributes));