# HG changeset patch
# User wenzelm
# Date 1566061443 -7200
# Node ID d94456876f2d3d5900588d241f1be39642eebb5b
# Parent  095dadc62bb536f3cbe7f34cfb85361531cdce28
clarified signature;

diff -r 095dadc62bb5 -r d94456876f2d src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sat Aug 17 17:59:55 2019 +0200
+++ b/src/Pure/Pure.thy	Sat Aug 17 19:04:03 2019 +0200
@@ -1304,8 +1304,10 @@
   Outer_Syntax.command \<^command_keyword>\<open>thm_deps\<close> "visualize theorem dependencies"
     (Parse.thms1 >> (fn args =>
       Toplevel.keep (fn st =>
-        Thm_Deps.thm_deps (Toplevel.theory_of st)
-          (Attrib.eval_thms (Toplevel.context_of st) args))));
+        let
+          val thy = Toplevel.theory_of st;
+          val ctxt = Toplevel.context_of st;
+        in Thm_Deps.thm_deps_cmd thy (Attrib.eval_thms ctxt args) end)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>thm_oracles\<close>
@@ -1329,7 +1331,7 @@
             fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
             val check = Theory.check {long = false} ctxt;
           in
-            Thm_Deps.unused_thms
+            Thm_Deps.unused_thms_cmd
               (case opt_range of
                 NONE => (Theory.parents_of thy, [thy])
               | SOME (xs, NONE) => (map check xs, [thy])
diff -r 095dadc62bb5 -r d94456876f2d src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Sat Aug 17 17:59:55 2019 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Sat Aug 17 19:04:03 2019 +0200
@@ -10,8 +10,8 @@
   val all_oracles: thm list -> Proofterm.oracle list
   val has_skip_proof: thm list -> bool
   val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
-  val thm_deps: theory -> thm list -> unit
-  val unused_thms: theory list * theory list -> (string * thm) list
+  val thm_deps_cmd: theory -> thm list -> unit
+  val unused_thms_cmd: theory list * theory list -> (string * thm) list
 end;
 
 structure Thm_Deps: THM_DEPS =
@@ -35,9 +35,9 @@
   in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end;
 
 
-(* thm_deps *)
+(* thm_deps_cmd *)
 
-fun thm_deps thy thms =
+fun thm_deps_cmd thy thms =
   let
     fun make_node name directory =
       Graph_Display.session_node
@@ -70,9 +70,9 @@
   end;
 
 
-(* unused_thms *)
+(* unused_thms_cmd *)
 
-fun unused_thms (base_thys, thys) =
+fun unused_thms_cmd (base_thys, thys) =
   let
     fun add_fact transfer space (name, ths) =
       if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I