src/HOL/Tools/datatype_realizer.ML
changeset 28814 463c9e9111ae
parent 28799 ee65e7d043fc
child 29579 cb520b766e00
--- a/src/HOL/Tools/datatype_realizer.ML	Sun Nov 16 18:19:27 2008 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Sun Nov 16 20:03:42 2008 +0100
@@ -27,8 +27,7 @@
   in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
 
 fun prf_of thm =
-  Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm)
-    (Proofterm.proof_of (Thm.proof_of thm));
+  Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
 
 fun prf_subst_vars inst =
   Proofterm.map_proof_terms (subst_vars ([], inst)) I;