# HG changeset patch
# User wenzelm
# Date 1331905573 -3600
# Node ID f19e5837ad6907fc479d40fcc9292bd3734f8dda
# Parent  cdc79191046025d0085042e5555680b675d216d5
refute_params are given in *this* theory;

diff -r cdc791910460 -r f19e5837ad69 src/HOL/Refute.thy
--- 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                                                                    *)
diff -r cdc791910460 -r f19e5837ad69 src/HOL/Tools/refute.ML
--- 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},