diff -r 0cc3ff184282 -r 64ee6a2ca6d6 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Feb 28 16:54:56 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Feb 28 17:33:35 2008 +0100
@@ -924,6 +924,12 @@
       (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
         (Code.print_codesetup o Toplevel.theory_of)));
 
+val _ =
+  OuterSyntax.improper_command "unused_thms" "find unused theorems" K.diag
+    (Scan.option ((Scan.repeat1 (Scan.unless P.minus P.name) --| P.minus) --
+       Scan.option (Scan.repeat1 (Scan.unless P.minus P.name))) >>
+         (Toplevel.no_timing oo IsarCmd.unused_thms));
+
 
 (** system commands (for interactive mode only) **)