src/HOL/Tools/datatype_realizer.ML
changeset 26626 c6231d64d264
parent 26481 92e901171cc8
child 28799 ee65e7d043fc
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Thu Apr 10 20:54:18 2008 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sat Apr 12 17:00:35 2008 +0200
     1.3 @@ -27,8 +27,7 @@
     1.4    in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
     1.5  
     1.6  fun prf_of thm =
     1.7 -  let val {thy, prop, der = (_, prf), ...} = rep_thm thm
     1.8 -  in Reconstruct.reconstruct_proof thy prop prf end;
     1.9 +  Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
    1.10  
    1.11  fun prf_subst_vars inst =
    1.12    Proofterm.map_proof_terms (subst_vars ([], inst)) I;