# HG changeset patch
# User wenzelm
# Date 1429218982 -7200
# Node ID d6b043ad7b3dce3741a83484963dd92b9dab28bb
# Parent  820e8e704ba6ceac70955fe2084ba88a109668d0
proper Theory.check;

diff -r 820e8e704ba6 -r d6b043ad7b3d src/Pure/Tools/thm_deps.ML
--- a/src/Pure/Tools/thm_deps.ML	Thu Apr 16 23:01:33 2015 +0200
+++ b/src/Pure/Tools/thm_deps.ML	Thu Apr 16 23:16:22 2015 +0200
@@ -104,22 +104,24 @@
       else q) new_thms ([], Inttab.empty);
   in rev thms' end;
 
+val thy_names =
+  Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
+
 val _ =
   Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
-    (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
-       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> (fn opt_range =>
-        Toplevel.keep (fn state =>
+    (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range =>
+        Toplevel.keep (fn st =>
           let
-            val thy = Toplevel.theory_of state;
-            val ctxt = Toplevel.context_of state;
+            val thy = Toplevel.theory_of st;
+            val ctxt = Toplevel.context_of st;
             fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
-            val get_theory = Context.get_theory thy;
+            val check = Theory.check ctxt;
           in
             unused_thms
               (case opt_range of
                 NONE => (Theory.parents_of thy, [thy])
-              | SOME (xs, NONE) => (map get_theory xs, [thy])
-              | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
+              | SOME (xs, NONE) => (map check xs, [thy])
+              | SOME (xs, SOME ys) => (map check xs, map check ys))
             |> map pretty_thm |> Pretty.writeln_chunks
           end)));