# HG changeset patch
# User kleing
# Date 1173155483 -3600
# Node ID c310ca7cd47fb76f66f411c28d25eaeef148f8b0
# Parent  3f189ea9bfe76a64845108db3fb8da08902952e2
find_theorems: moved with_dup into the brackets, i.e.

find_theorems (20 with_dups) "some term" ..

diff -r 3f189ea9bfe7 -r c310ca7cd47f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Mar 06 05:09:53 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 06 05:31:23 2007 +0100
@@ -809,8 +809,10 @@
 val find_theoremsP =
   OuterSyntax.improper_command "find_theorems"
     "print theorems meeting specified criteria" K.diag
-    (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
-     Scan.optional (P.reserved "with_dups" >> K false) true -- 
+    (Scan.optional (P.$$$ "(" |-- P.!!!
+                        (Scan.option P.nat --
+                         Scan.optional (P.reserved "with_dups" >> K false) true
+                         --| P.$$$ ")")) (NONE, false) --
      Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
       >> (Toplevel.no_timing oo IsarCmd.find_theorems));