src/HOL/Tools/refute.ML
changeset 17412 e26cb20ef0cc
parent 17314 04e21a27c0ad
child 17493 cf8713d880b1
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Sep 15 17:16:55 2005 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Sep 15 17:16:56 2005 +0200
     1.3 @@ -298,11 +298,11 @@
     1.4  	let
     1.5  		val {interpreters, printers, parameters} = RefuteData.get thy
     1.6  	in
     1.7 -		case Symtab.curried_lookup parameters name of
     1.8 +		case Symtab.lookup parameters name of
     1.9  		  NONE   => RefuteData.put
    1.10  			{interpreters = interpreters, printers = printers, parameters = Symtab.extend (parameters, [(name, value)])} thy
    1.11  		| SOME _ => RefuteData.put
    1.12 -			{interpreters = interpreters, printers = printers, parameters = Symtab.curried_update (name, value) parameters} thy
    1.13 +			{interpreters = interpreters, printers = printers, parameters = Symtab.update (name, value) parameters} thy
    1.14  	end;
    1.15  
    1.16  (* ------------------------------------------------------------------------- *)
    1.17 @@ -312,7 +312,7 @@
    1.18  
    1.19  	(* theory -> string -> string option *)
    1.20  
    1.21 -	val get_default_param = Symtab.curried_lookup o #parameters o RefuteData.get;
    1.22 +	val get_default_param = Symtab.lookup o #parameters o RefuteData.get;
    1.23  
    1.24  (* ------------------------------------------------------------------------- *)
    1.25  (* get_default_params: returns a list of all '(name, value)' pairs that are  *)