src/HOL/Tools/ATP/res_clasimpset.ML

 
 fun consts_in_goal goal = consts_of_term goal;
 
 fun axioms_having_consts_aux [] tab thms = thms
   | axioms_having_consts_aux (c::cs) tab thms =
-    let val thms1 = Symtab.lookup(tab,c)
-	val thms2 = 
-	    case thms1 of (SOME x) => x
-			| NONE => []
-    in
-	axioms_having_consts_aux cs tab (thms2 union thms)
-    end;
-
+    let val thms1 = Symtab.curried_lookup tab c
+      val thms2 = 
+          case thms1 of (SOME x) => x
+                      | NONE => []
+    in
+      axioms_having_consts_aux cs tab (thms2 union thms)
+    end;
 
 fun axioms_having_consts cs tab = axioms_having_consts_aux cs tab [];
 
 
 fun relevant_axioms goal thmTab n =