src/Pure/thm.ML

 
 (*look up the named axiom in the theory or its ancestors*)
 fun get_axiom_i theory name =
   let
     fun get_ax thy =
-      Symtab.lookup (#2 (#axioms (Theory.rep_theory thy)), name)
+      Symtab.curried_lookup (#2 (#axioms (Theory.rep_theory thy))) name
       |> Option.map (fn prop =>
           Thm {thy_ref = Theory.self_ref thy,
             der = Pt.infer_derivs' I (false, Pt.axm_proof name prop),
             maxidx = maxidx_of_term prop,
             shyps = may_insert_term_sorts thy prop [],

 (*** Oracles ***)
 
 fun invoke_oracle_i thy1 name =
   let
     val oracle =
-      (case Symtab.lookup (#2 (#oracles (Theory.rep_theory thy1)), name) of
+      (case Symtab.curried_lookup (#2 (#oracles (Theory.rep_theory thy1))) name of
         NONE => raise THM ("Unknown oracle: " ^ name, 0, [])
       | SOME (f, _) => f);
     val thy_ref1 = Theory.self_ref thy1;
   in
     fn (thy2, data) =>