src/HOL/Tools/refute.ML
changeset 17261 193b84a70ca4
parent 16935 4d7f19d340e8
child 17274 746bb4c56800
     1.1 --- a/src/HOL/Tools/refute.ML	Mon Sep 05 17:38:17 2005 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Mon Sep 05 17:38:18 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.lookup (parameters, name) of
     1.8 +		case Symtab.curried_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.update ((name, value), parameters)} thy
    1.13 +			{interpreters = interpreters, printers = printers, parameters = Symtab.curried_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 -	fun get_default_param thy name = Symtab.lookup ((#parameters o RefuteData.get) thy, name);
    1.22 +	val get_default_param = Symtab.curried_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  *)
    1.26 @@ -321,7 +321,7 @@
    1.27  
    1.28  	(* theory -> (string * string) list *)
    1.29  
    1.30 -	fun get_default_params thy = (Symtab.dest o #parameters o RefuteData.get) thy;
    1.31 +	val get_default_params = Symtab.dest o #parameters o RefuteData.get;
    1.32  
    1.33  (* ------------------------------------------------------------------------- *)
    1.34  (* actual_params: takes a (possibly empty) list 'params' of parameters that  *)