# HG changeset patch
# User blanchet
# Date 1300985367 -3600
# Node ID ed1d40888b1b5b5e84a2402fd088416b04f86329
# Parent  bba85afcfedf662a4882678c372a133565186e36
specify proper defaults for Nitpick and Refute on TPTP + tuning

diff -r bba85afcfedf -r ed1d40888b1b src/HOL/ex/TPTP.thy
--- a/src/HOL/ex/TPTP.thy	Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/ex/TPTP.thy	Thu Mar 24 17:49:27 2011 +0100
@@ -14,6 +14,10 @@
 
 declare [[smt_oracle]]
 
+refute_params [maxtime = 10000, no_assms, expect = genuine]
+nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms,
+                expect = genuine]
+
 ML {* Proofterm.proofs := 0 *}
 
 ML {*
diff -r bba85afcfedf -r ed1d40888b1b src/HOL/ex/sledgehammer_tactics.ML
--- a/src/HOL/ex/sledgehammer_tactics.ML	Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/ex/sledgehammer_tactics.ML	Thu Mar 24 17:49:27 2011 +0100
@@ -50,11 +50,6 @@
       handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
   end
 
-fun to_period ("." :: _) = []
-  | to_period ("" :: ss) = to_period ss
-  | to_period (s :: ss) = s :: to_period ss
-  | to_period [] = []
-
 val atp = "e" (* or "vampire" or "spass" etc. *)
 
 fun thms_of_name ctxt name =