src/HOL/Tools/primrec_package.ML

 
 (* find datatypes which contain all datatypes in tnames' *)
 
 fun find_dts (dt_info : datatype_info Symtab.table) _ [] = []
   | find_dts dt_info tnames' (tname::tnames) =
-      (case Symtab.curried_lookup dt_info tname of
+      (case Symtab.lookup dt_info tname of
           NONE => primrec_err (quote tname ^ " is not a datatype")
         | SOME dt =>
             if tnames' subset (map (#1 o snd) (#descr dt)) then
               (tname, dt)::(find_dts dt_info tnames' tnames)
             else find_dts dt_info tnames' tnames);