# HG changeset patch
# User blanchet
# Date 1301917316 -7200
# Node ID b33d871675bb8a61b4c0544c9614d90418a589be
# Parent  8de8c38d503b05705d71e30d6fd777da8f53219d# Parent  9e2673711c778166bd1a5aa949ffd4aaf11bfcb7
merged

diff -r 8de8c38d503b -r b33d871675bb src/HOL/ex/TPTP.thy
--- a/src/HOL/ex/TPTP.thy	Mon Apr 04 12:40:00 2011 +0100
+++ b/src/HOL/ex/TPTP.thy	Mon Apr 04 13:41:56 2011 +0200
@@ -16,7 +16,7 @@
 
 refute_params [maxtime = 10000, no_assms, expect = genuine]
 nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms,
-                expect = genuine]
+                batch_size = 1, expect = genuine]
 
 ML {* Proofterm.proofs := 0 *}