--- a/src/Pure/Proof/proofchecker.ML Thu Sep 15 17:16:55 2005 +0200
+++ b/src/Pure/Proof/proofchecker.ML Thu Sep 15 17:16:56 2005 +0200
@@ -19,9 +19,9 @@
(***** construct a theorem out of a proof term *****)
fun lookup_thm thy =
- let val tab = fold_rev Symtab.curried_update (PureThy.all_thms_of thy) Symtab.empty
+ let val tab = fold_rev Symtab.update (PureThy.all_thms_of thy) Symtab.empty
in
- (fn s => case Symtab.curried_lookup tab s of
+ (fn s => case Symtab.lookup tab s of
NONE => error ("Unknown theorem " ^ quote s)
| SOME thm => thm)
end;