src/HOL/Tools/refute.ML
changeset 29004 a5a91f387791
parent 28524 644b62cf678f
child 29265 5b4247055bd7
     1.1 --- a/src/HOL/Tools/refute.ML	Fri Dec 05 11:42:27 2008 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Dec 05 18:42:37 2008 +0100
     1.3 @@ -313,18 +313,10 @@
     1.4  
     1.5    (* (string * string) -> theory -> theory *)
     1.6  
     1.7 -  fun set_default_param (name, value) thy =
     1.8 -  let
     1.9 -    val {interpreters, printers, parameters} = RefuteData.get thy
    1.10 -  in
    1.11 -    RefuteData.put (case Symtab.lookup parameters name of
    1.12 -      NONE   =>
    1.13 +  fun set_default_param (name, value) = RefuteData.map 
    1.14 +    (fn {interpreters, printers, parameters} =>
    1.15        {interpreters = interpreters, printers = printers,
    1.16 -        parameters = Symtab.extend (parameters, [(name, value)])}
    1.17 -    | SOME _ =>
    1.18 -      {interpreters = interpreters, printers = printers,
    1.19 -        parameters = Symtab.update (name, value) parameters}) thy
    1.20 -  end;
    1.21 +        parameters = Symtab.update (name, value) parameters});
    1.22  
    1.23  (* ------------------------------------------------------------------------- *)
    1.24  (* get_default_param: retrieves the value associated with 'name' from        *)