src/Pure/Proof/extraction.ML

 
       | extr d defs vs ts Ts hs _ = error "extr: bad proof";
 
     fun prep_thm (thm, vs) =
       let
-        val {prop, der = (_, prf), thy, ...} = rep_thm thm;
+        val thy = Thm.theory_of_thm thm;
+        val prop = Thm.prop_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 " ^
           quote name ^ " has no computational content")
       in (Reconstruct.reconstruct_proof thy prop prf, vs) end;