src/Pure/Proof/proofchecker.ML

--- a/src/Pure/Proof/proofchecker.ML	Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Proof/proofchecker.ML	Mon Sep 20 16:05:25 2010 +0200
@@ -16,7 +16,7 @@
 (***** construct a theorem out of a proof term *****)
 
 fun lookup_thm thy =
-  let val tab = fold_rev Symtab.update (PureThy.all_thms_of thy) Symtab.empty
+  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty
   in
     (fn s => case Symtab.lookup tab s of
        NONE => error ("Unknown theorem " ^ quote s)