# HG changeset patch
# User wenzelm
# Date 1118311418 -7200
# Node ID 561b9f8be72e568e5e22ce1960ecc0ec1b2adc7c
# Parent  caa9b780ad91328c1ff9d1d6673565c3a02c2500
PureThy.all_thms_of;

diff -r caa9b780ad91 -r 561b9f8be72e src/Pure/Proof/proofchecker.ML
--- 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)