--- a/src/HOL/Tools/refute.ML Fri Dec 05 11:42:27 2008 +0100
+++ b/src/HOL/Tools/refute.ML Fri Dec 05 18:42:37 2008 +0100
@@ -313,18 +313,10 @@
(* (string * string) -> theory -> theory *)
- fun set_default_param (name, value) thy =
- let
- val {interpreters, printers, parameters} = RefuteData.get thy
- in
- RefuteData.put (case Symtab.lookup parameters name of
- NONE =>
+ fun set_default_param (name, value) = RefuteData.map
+ (fn {interpreters, printers, parameters} =>
{interpreters = interpreters, printers = printers,
- parameters = Symtab.extend (parameters, [(name, value)])}
- | SOME _ =>
- {interpreters = interpreters, printers = printers,
- parameters = Symtab.update (name, value) parameters}) thy
- end;
+ parameters = Symtab.update (name, value) parameters});
(* ------------------------------------------------------------------------- *)
(* get_default_param: retrieves the value associated with 'name' from *)