# HG changeset patch
# User wenzelm
# Date 1208375582 -7200
# Node ID 29f5c1a296bc55f7f094d6db40a3883a5be5731a
# Parent  90d0b86644ac215a36259f0103a9c6871f590795
PureThy.defined_fact;
unused_thms: simplified signature;

diff -r 90d0b86644ac -r 29f5c1a296bc src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Apr 16 21:53:01 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Apr 16 21:53:02 2008 +0200
@@ -259,7 +259,7 @@
  [("class", (Sign.intern_class, can o Sign.certify_class, Sign.hide_class)),
   ("type", (Sign.intern_type, Sign.declared_tyname, Sign.hide_type)),
   ("const", (Sign.intern_const, Sign.declared_const, Sign.hide_const)),
-  ("fact", (PureThy.intern_fact, PureThy.check_fact, PureThy.hide_fact))];
+  ("fact", (PureThy.intern_fact, PureThy.defined_fact, PureThy.hide_fact))];
 
 fun hide_names b (kind, xnames) thy =
   (case AList.lookup (op =) hide_kinds kind of
@@ -552,9 +552,9 @@
   in
     ThmDeps.unused_thms
       (case opt_range of
-         NONE => (NONE, [thy])
-       | SOME (xs, NONE) => (SOME (map ThyInfo.get_theory xs), [thy])
-       | SOME (xs, SOME ys) => (SOME (map ThyInfo.get_theory xs), map ThyInfo.get_theory ys))
+        NONE => (Theory.parents_of thy, [thy])
+      | SOME (xs, NONE) => (map ThyInfo.get_theory xs, [thy])
+      | SOME (xs, SOME ys) => (map ThyInfo.get_theory xs, map ThyInfo.get_theory ys))
     |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
   end);