1.1 --- a/src/HOL/Refute.thy	Fri Mar 16 14:42:11 2012 +0100
     1.2 +++ b/src/HOL/Refute.thy	Fri Mar 16 14:46:13 2012 +0100
     1.3 @@ -15,6 +15,15 @@
     1.4  
     1.5  setup Refute.setup
     1.6  
     1.7 +refute_params
     1.8 + [itself = 1,
     1.9 +  minsize = 1,
    1.10 +  maxsize = 8,
    1.11 +  maxvars = 10000,
    1.12 +  maxtime = 60,
    1.13 +  satsolver = auto,
    1.14 +  no_assms = false]
    1.15 +
    1.16  text {*
    1.17  \small
    1.18  \begin{verbatim}
    1.19 @@ -80,8 +89,6 @@
    1.20  (* "expect"      string  Expected result ("genuine", "potential", "none", or *)
    1.21  (*                       "unknown").                                         *)
    1.22  (*                                                                           *)
    1.23 -(* See 'HOL/SAT.thy' for default values.                                     *)
    1.24 -(*                                                                           *)
    1.25  (* The size of particular types can be specified in the form type=size       *)
    1.26  (* (where 'type' is a string, and 'size' is an int).  Examples:              *)
    1.27  (* "'a"=1                                                                    *)

     2.1 --- a/src/HOL/Tools/refute.ML	Fri Mar 16 14:42:11 2012 +0100
     2.2 +++ b/src/HOL/Tools/refute.ML	Fri Mar 16 14:46:13 2012 +0100
     2.3 @@ -204,16 +204,6 @@
     2.4      wellformed: prop_formula
     2.5    };
     2.6  
     2.7 -val default_parameters =
     2.8 - [("itself", "1"),
     2.9 -  ("minsize", "1"),
    2.10 -  ("maxsize", "8"),
    2.11 -  ("maxvars", "10000"),
    2.12 -  ("maxtime", "60"),
    2.13 -  ("satsolver", "auto"),
    2.14 -  ("no_assms", "false")]
    2.15 - |> Symtab.make
    2.16 -
    2.17  structure Data = Theory_Data
    2.18  (
    2.19    type T =
    2.20 @@ -222,8 +212,7 @@
    2.21       printers: (string * (Proof.context -> model -> typ -> interpretation ->
    2.22        (int -> bool) -> term option)) list,
    2.23       parameters: string Symtab.table};
    2.24 -  val empty =
    2.25 -    {interpreters = [], printers = [], parameters = default_parameters};
    2.26 +  val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
    2.27    val extend = I;
    2.28    fun merge
    2.29      ({interpreters = in1, printers = pr1, parameters = pa1},