find_theorems: moved with_dup into the brackets, i.e.
authorkleing
Tue Mar 06 05:31:23 2007 +0100 (2007-03-06 ago)
changeset 22415c310ca7cd47f
parent 22414 3f189ea9bfe7
child 22416 4af50522be35
find_theorems: moved with_dup into the brackets, i.e.

find_theorems (20 with_dups) "some term" ..
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Mar 06 05:09:53 2007 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 06 05:31:23 2007 +0100
     1.3 @@ -809,8 +809,10 @@
     1.4  val find_theoremsP =
     1.5    OuterSyntax.improper_command "find_theorems"
     1.6      "print theorems meeting specified criteria" K.diag
     1.7 -    (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
     1.8 -     Scan.optional (P.reserved "with_dups" >> K false) true -- 
     1.9 +    (Scan.optional (P.$$$ "(" |-- P.!!!
    1.10 +                        (Scan.option P.nat --
    1.11 +                         Scan.optional (P.reserved "with_dups" >> K false) true
    1.12 +                         --| P.$$$ ")")) (NONE, false) --
    1.13       Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
    1.14        >> (Toplevel.no_timing oo IsarCmd.find_theorems));
    1.15