Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Proof/proof_syntax.ML
changeset 13530 4813fdc0ef17
parent 13199 18402c1f76bf
child 14854 61bdf2ae4dc5 
--- a/src/Pure/Proof/proof_syntax.ML	Tue Aug 27 11:06:07 2002 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Aug 27 11:06:20 2002 +0200
@@ -147,7 +147,7 @@
              | "thm" :: xs =>
                  let val name = NameSpace.pack xs;
                  in (case assoc (thms, name) of
-                     Some thm => fst (strip_combt (#2 (#der (rep_thm thm))))
+                     Some thm => fst (strip_combt (Thm.proof_of thm))
                    | None => (case Symtab.lookup (tab, name) of
                          Some prf => prf
                        | None => error ("Unknown theorem " ^ quote name)))
isabelle