--- a/src/Pure/Tools/find_theorems.ML Fri Mar 16 14:46:13 2012 +0100
+++ b/src/Pure/Tools/find_theorems.ML Fri Mar 16 18:20:12 2012 +0100
@@ -612,8 +612,8 @@
val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
val _ =
- Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria"
- Keyword.diag
+ Outer_Syntax.improper_command ("find_theorems", Keyword.diag)
+ "print theorems meeting specified criteria"
(options -- query_parser
>> (fn ((opt_lim, rem_dups), spec) =>
Toplevel.no_timing o