src/Pure/Tools/find_theorems.ML
changeset 48646 91281e9472d8
parent 46977 bd0ee92cabe7
child 49888 ff2063be8227
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Aug 02 11:32:23 2012 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Aug 02 12:36:54 2012 +0200
     1.3 @@ -615,7 +615,7 @@
     1.4  val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.improper_command ("find_theorems", Keyword.diag)
     1.8 +  Outer_Syntax.improper_command @{command_spec "find_theorems"}
     1.9      "print theorems meeting specified criteria"
    1.10      (options -- query_parser
    1.11        >> (fn ((opt_lim, rem_dups), spec) =>