src/Pure/Proof/proof_checker.ML

 struct
 
 (***** construct a theorem out of a proof term *****)
 
 fun lookup_thm thy =
-  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty in
+  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy true) Symtab.empty in
     fn s =>
       (case Symtab.lookup tab s of
         NONE => error ("Unknown theorem " ^ quote s)
       | SOME thm => thm)
   end;