src/HOL/Tools/refute.ML
changeset 46960 f19e5837ad69
parent 46949 94aa7b81bcf6
child 46961 5c6955f487e5
     1.1 --- a/src/HOL/Tools/refute.ML	Fri Mar 16 14:42:11 2012 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Mar 16 14:46:13 2012 +0100
     1.3 @@ -204,16 +204,6 @@
     1.4      wellformed: prop_formula
     1.5    };
     1.6  
     1.7 -val default_parameters =
     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 - |> Symtab.make
    1.16 -
    1.17  structure Data = Theory_Data
    1.18  (
    1.19    type T =
    1.20 @@ -222,8 +212,7 @@
    1.21       printers: (string * (Proof.context -> model -> typ -> interpretation ->
    1.22        (int -> bool) -> term option)) list,
    1.23       parameters: string Symtab.table};
    1.24 -  val empty =
    1.25 -    {interpreters = [], printers = [], parameters = default_parameters};
    1.26 +  val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
    1.27    val extend = I;
    1.28    fun merge
    1.29      ({interpreters = in1, printers = pr1, parameters = pa1},