src/HOL/Tools/ATP/res_clasimpset.ML
changeset 17261 193b84a70ca4
parent 17234 12a9393c5d77
child 17305 6cef3aedd661
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Mon Sep 05 17:38:17 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Mon Sep 05 17:38:18 2005 +0200
     1.3 @@ -57,15 +57,14 @@
     1.4  
     1.5  fun axioms_having_consts_aux [] tab thms = thms
     1.6    | axioms_having_consts_aux (c::cs) tab thms =
     1.7 -    let val thms1 = Symtab.lookup(tab,c)
     1.8 -	val thms2 = 
     1.9 -	    case thms1 of (SOME x) => x
    1.10 -			| NONE => []
    1.11 +    let val thms1 = Symtab.curried_lookup tab c
    1.12 +      val thms2 = 
    1.13 +          case thms1 of (SOME x) => x
    1.14 +                      | NONE => []
    1.15      in
    1.16 -	axioms_having_consts_aux cs tab (thms2 union thms)
    1.17 +      axioms_having_consts_aux cs tab (thms2 union thms)
    1.18      end;
    1.19  
    1.20 -
    1.21  fun axioms_having_consts cs tab = axioms_having_consts_aux cs tab [];
    1.22  
    1.23