src/HOL/Integ/cooper_proof.ML
changeset 17485 c39871c52977
parent 16389 48832eba5b1e
child 17959 8db36a108213
     1.1 --- a/src/HOL/Integ/cooper_proof.ML	Mon Sep 19 15:12:13 2005 +0200
     1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Mon Sep 19 16:38:35 2005 +0200
     1.3 @@ -787,7 +787,7 @@
     1.4  
     1.5  fun rho_for_evalc sg at = case at of  
     1.6      (Const (p,_) $ s $ t) =>(  
     1.7 -    case assoc (operations,p) of 
     1.8 +    case AList.lookup (op =) operations p of 
     1.9          SOME f => 
    1.10             ((if (f ((dest_numeral s),(dest_numeral t))) 
    1.11               then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)) 
    1.12 @@ -795,7 +795,7 @@
    1.13  		   handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl)
    1.14          | _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl )
    1.15       |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
    1.16 -       case assoc (operations,p) of 
    1.17 +       case AList.lookup (op =) operations p of 
    1.18           SOME f => 
    1.19             ((if (f ((dest_numeral s),(dest_numeral t))) 
    1.20               then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))