--- a/src/Pure/Proof/proofchecker.ML Thu Jun 09 12:03:37 2005 +0200
+++ b/src/Pure/Proof/proofchecker.ML Thu Jun 09 12:03:38 2005 +0200
@@ -19,8 +19,7 @@
(***** construct a theorem out of a proof term *****)
fun lookup_thm thy =
- let val tab = foldr Symtab.update Symtab.empty
- (List.concat (map thms_of (thy :: Theory.ancestors_of thy)))
+ let val tab = foldr Symtab.update Symtab.empty (PureThy.all_thms_of thy)
in
(fn s => case Symtab.lookup (tab, s) of
NONE => error ("Unknown theorem " ^ quote s)