# HG changeset patch
# User wenzelm
# Date 1429193979 -7200
# Node ID 3c66b0a9d7b0f625ce3391d334c8e8e3ce8947d8
# Parent  d20ca79d50e4ca7262e0fde89eb79db75f943198
tuned;

diff -r d20ca79d50e4 -r 3c66b0a9d7b0 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 15:22:44 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 16:19:39 2015 +0200
@@ -35,7 +35,6 @@
   val diag_state: Proof.context -> Toplevel.state
   val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
   val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
-  val locale_deps: Toplevel.transition -> Toplevel.transition
   val print_stmts: string list * (Facts.ref * Token.src list) list
     -> Toplevel.transition -> Toplevel.transition
   val print_thms: string list * (Facts.ref * Token.src list) list
@@ -264,16 +263,6 @@
     in Proof_Display.pretty_theorems_diff verbose prev_thys thy end;
 
 
-(* display dependencies *)
-
-val locale_deps =
-  Toplevel.keep (Toplevel.theory_of #> (fn thy =>
-    Locale.pretty_locale_deps thy
-    |> map (fn {name, parents, body} =>
-      ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
-    |> Graph_Display.display_graph));
-
-
 (* print theorems, terms, types etc. *)
 
 local
diff -r d20ca79d50e4 -r 3c66b0a9d7b0 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Apr 16 15:22:44 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Apr 16 16:19:39 2015 +0200
@@ -789,7 +789,12 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies"
-    (Scan.succeed Isar_Cmd.locale_deps);
+    (Scan.succeed
+      (Toplevel.keep (Toplevel.theory_of #> (fn thy =>
+        Locale.pretty_locale_deps thy
+        |> map (fn {name, parents, body} =>
+          ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
+        |> Graph_Display.display_graph))));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_term_bindings}