src/HOL/Integ/reflected_cooper.ML
changeset 17521 0f1c48de39f5
parent 17427 3c45d890d47c
child 19233 77ca20b0ed77
     1.1 --- a/src/HOL/Integ/reflected_cooper.ML	Tue Sep 20 15:12:40 2005 +0200
     1.2 +++ b/src/HOL/Integ/reflected_cooper.ML	Tue Sep 20 16:17:34 2005 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  fun i_of_term vs t = 
     1.6      case t of
     1.7 -	Free(xn,xT) => (case assoc(vs,t) of 
     1.8 +	Free(xn,xT) => (case AList.lookup (op =) vs t of 
     1.9  			   NONE   => error "Variable not found in the list!!"
    1.10  			 | SOME n => Var n)
    1.11        | Const("0",iT) => Cst 0