src/Pure/Tools/find_theorems.ML
changeset 43068 ac769b5edd1d
parent 43067 76e1d25c6357
child 43069 88e45168272c
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4    val limit: int Unsynchronized.ref
     1.5  
     1.6    val read_criterion: Proof.context -> string criterion -> term criterion
     1.7 +  val query_parser: (bool * string criterion) list parser
     1.8  
     1.9    val find_theorems: Proof.context -> thm option -> int option -> bool ->
    1.10      (bool * term criterion) list -> int option * (Facts.ref * thm) list
    1.11 @@ -530,10 +531,12 @@
    1.12          --| Parse.$$$ ")")) (NONE, true);
    1.13  in
    1.14  
    1.15 +val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
    1.16 +
    1.17  val _ =
    1.18    Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria"
    1.19      Keyword.diag
    1.20 -    (options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion))
    1.21 +    (options -- query_parser
    1.22        >> (fn ((opt_lim, rem_dups), spec) =>
    1.23          Toplevel.no_timing o
    1.24          Toplevel.keep (fn state =>