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/extraction.ML
changeset 28814 463c9e9111ae
parent 28812 413695e07bd4
child 29265 5b4247055bd7 
--- a/src/Pure/Proof/extraction.ML	Sun Nov 16 18:19:27 2008 +0100
+++ b/src/Pure/Proof/extraction.ML	Sun Nov 16 20:03:42 2008 +0100
@@ -714,7 +714,7 @@
       let
         val thy = Thm.theory_of_thm thm;
         val prop = Thm.prop_of thm;
-        val prf = proof_of (Thm.proof_of thm);
+        val prf = Thm.proof_of thm;
         val name = Thm.get_name thm;
         val _ = name <> "" orelse error "extraction: unnamed theorem";
         val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
isabelle