src/HOL/SAT.thy

--- a/src/HOL/SAT.thy	Tue Jan 03 18:33:18 2012 +0100
+++ b/src/HOL/SAT.thy	Tue Jan 03 18:33:18 2012 +0100
@@ -13,18 +13,6 @@
   "Tools/sat_funcs.ML"
 begin
 
-text {* \medskip Late package setup: default values for refute, see
-  also theory @{theory Refute}. *}
-
-refute_params
- ["itself"=1,
-  minsize=1,
-  maxsize=8,
-  maxvars=10000,
-  maxtime=60,
-  satsolver="auto",
-  no_assms="false"]
-
 ML {* structure sat = SATFunc(cnf) *}
 
 method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *}