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