--- 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 {*
--- 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 =