src/Pure/Proof/extraction.ML
changeset 26626 c6231d64d264
parent 26481 92e901171cc8
child 26653 60e0cf6bef89
     1.1 --- a/src/Pure/Proof/extraction.ML	Thu Apr 10 20:54:18 2008 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sat Apr 12 17:00:35 2008 +0200
     1.3 @@ -711,7 +711,9 @@
     1.4  
     1.5      fun prep_thm (thm, vs) =
     1.6        let
     1.7 -        val {prop, der = (_, prf), thy, ...} = rep_thm thm;
     1.8 +        val thy = Thm.theory_of_thm thm;
     1.9 +        val prop = Thm.prop_of thm;
    1.10 +        val prf = Thm.proof_of thm;
    1.11          val name = Thm.get_name thm;
    1.12          val _ = name <> "" orelse error "extraction: unnamed theorem";
    1.13          val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^