1.1 --- a/src/Pure/Proof/proof_syntax.ML	Tue Aug 27 11:06:07 2002 +0200
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Tue Aug 27 11:06:20 2002 +0200
     1.3 @@ -147,7 +147,7 @@
     1.4               | "thm" :: xs =>
     1.5                   let val name = NameSpace.pack xs;
     1.6                   in (case assoc (thms, name) of
     1.7 -                     Some thm => fst (strip_combt (#2 (#der (rep_thm thm))))
     1.8 +                     Some thm => fst (strip_combt (Thm.proof_of thm))
     1.9                     | None => (case Symtab.lookup (tab, name) of
    1.10                           Some prf => prf
    1.11                         | None => error ("Unknown theorem " ^ quote name)))