--- a/src/HOL/Refute.thy Fri Mar 16 14:42:11 2012 +0100
+++ b/src/HOL/Refute.thy Fri Mar 16 14:46:13 2012 +0100
@@ -15,6 +15,15 @@
setup Refute.setup
+refute_params
+ [itself = 1,
+ minsize = 1,
+ maxsize = 8,
+ maxvars = 10000,
+ maxtime = 60,
+ satsolver = auto,
+ no_assms = false]
+
text {*
\small
\begin{verbatim}
@@ -80,8 +89,6 @@
(* "expect" string Expected result ("genuine", "potential", "none", or *)
(* "unknown"). *)
(* *)
-(* See 'HOL/SAT.thy' for default values. *)
-(* *)
(* The size of particular types can be specified in the form type=size *)
(* (where 'type' is a string, and 'size' is an int). Examples: *)
(* "'a"=1 *)
--- a/src/HOL/Tools/refute.ML Fri Mar 16 14:42:11 2012 +0100
+++ b/src/HOL/Tools/refute.ML Fri Mar 16 14:46:13 2012 +0100
@@ -204,16 +204,6 @@
wellformed: prop_formula
};
-val default_parameters =
- [("itself", "1"),
- ("minsize", "1"),
- ("maxsize", "8"),
- ("maxvars", "10000"),
- ("maxtime", "60"),
- ("satsolver", "auto"),
- ("no_assms", "false")]
- |> Symtab.make
-
structure Data = Theory_Data
(
type T =
@@ -222,8 +212,7 @@
printers: (string * (Proof.context -> model -> typ -> interpretation ->
(int -> bool) -> term option)) list,
parameters: string Symtab.table};
- val empty =
- {interpreters = [], printers = [], parameters = default_parameters};
+ val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
val extend = I;
fun merge
({interpreters = in1, printers = pr1, parameters = pa1},