--- a/src/Pure/Proof/proofchecker.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/Proof/proofchecker.ML Fri Mar 04 15:07:34 2005 +0100
@@ -19,8 +19,8 @@
(***** construct a theorem out of a proof term *****)
fun lookup_thm thy =
- let val tab = Library.foldr Symtab.update
- (List.concat (map thms_of (thy :: Theory.ancestors_of thy)), Symtab.empty)
+ let val tab = foldr Symtab.update Symtab.empty
+ (List.concat (map thms_of (thy :: Theory.ancestors_of thy)))
in
(fn s => case Symtab.lookup (tab, s) of
NONE => error ("Unknown theorem " ^ quote s)