src/Pure/Tools/find_theorems.ML
changeset 46961 5c6955f487e5
parent 46718 dfaf51de90ad
child 46977 bd0ee92cabe7
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Mar 16 14:46:13 2012 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Mar 16 18:20:12 2012 +0100
     1.3 @@ -612,8 +612,8 @@
     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" "print theorems meeting specified criteria"
     1.8 -    Keyword.diag
     1.9 +  Outer_Syntax.improper_command ("find_theorems", Keyword.diag)
    1.10 +    "print theorems meeting specified criteria"
    1.11      (options -- query_parser
    1.12        >> (fn ((opt_lim, rem_dups), spec) =>
    1.13          Toplevel.no_timing o