src/HOL/Tools/refute.ML
changeset 14460 04e787a4f17a
parent 14456 cca28ec5f9a6
child 14488 863258b0cdca
     1.1 --- a/src/HOL/Tools/refute.ML	Wed Mar 10 22:39:12 2004 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Mar 11 00:15:24 2004 +0100
     1.3 @@ -686,7 +686,7 @@
     1.4  
     1.5  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
     1.6  
     1.7 -	fun boundvar_interpreter thy model args (Bound i) = Some (nth_elem (i, #bounds args), model, args)
     1.8 +	fun boundvar_interpreter thy model args (Bound i) = Some (nth_elem (i, #bounds (args:arguments)), model, args)
     1.9  	  | boundvar_interpreter thy model args _         = None;
    1.10  
    1.11  	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)