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