src/HOL/Tools/datatype_realizer.ML
changeset 28814 463c9e9111ae
parent 28799 ee65e7d043fc
child 29579 cb520b766e00
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Sun Nov 16 18:19:27 2008 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sun Nov 16 20:03:42 2008 +0100
     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 -  Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm)
     1.8 -    (Proofterm.proof_of (Thm.proof_of thm));
     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;