--- a/src/Pure/thm.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/thm.ML Thu Sep 01 18:48:50 2005 +0200
@@ -524,7 +524,7 @@
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),
@@ -1482,7 +1482,7 @@
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;