1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Feb 28 16:54:56 2008 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Feb 28 17:33:35 2008 +0100
     1.3 @@ -924,6 +924,12 @@
     1.4        (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
     1.5          (Code.print_codesetup o Toplevel.theory_of)));
     1.6  
     1.7 +val _ =
     1.8 +  OuterSyntax.improper_command "unused_thms" "find unused theorems" K.diag
     1.9 +    (Scan.option ((Scan.repeat1 (Scan.unless P.minus P.name) --| P.minus) --
    1.10 +       Scan.option (Scan.repeat1 (Scan.unless P.minus P.name))) >>
    1.11 +         (Toplevel.no_timing oo IsarCmd.unused_thms));
    1.12 +
    1.13  
    1.14  (** system commands (for interactive mode only) **)
    1.15