# HG changeset patch
# User wenzelm
# Date 1204221562 -3600
# Node ID 9af968b694d94aa96992b9a54ca33e2cdb2242f5
# Parent  e531653193473b813b690eae817f8526595da870
unused_thms: print via official context (ProofContext.pretty_fact),
  not just the theory certificate (Display.pretty_thm);
tuned;

diff -r e53165319347 -r 9af968b694d9 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Feb 28 17:34:15 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Feb 28 18:59:22 2008 +0100
@@ -535,24 +535,19 @@
 
 (* find unused theorems *)
 
-local
-
-fun pretty_name_thm (a, th) =
-  Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, Display.pretty_thm th];
-
-in
-
-fun unused_thms opt_range =
-  Toplevel.keep (fn state => ThmDeps.unused_thms
-    (case opt_range of
-       NONE => (NONE, [Toplevel.theory_of state])
-     | SOME (xs, NONE) =>
-         (SOME (map ThyInfo.get_theory xs), [Toplevel.theory_of state])
-     | SOME (xs, SOME ys) =>
-        (SOME (map ThyInfo.get_theory xs), map ThyInfo.get_theory ys)) |>
-           map pretty_name_thm |> Pretty.chunks |> Pretty.writeln);
-
-end;        
+fun unused_thms opt_range = Toplevel.keep (fn state =>
+  let
+    val thy = Toplevel.theory_of state;
+    val ctxt = Toplevel.context_of state;
+    fun pretty_thm (a, th) = ProofContext.pretty_fact ctxt (a, [th]);
+  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))
+    |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
+  end);
 
 
 (* print proof context contents *)