Thm.proof_of returns proof_body;
authorwenzelm
Sat Nov 15 21:31:17 2008 +0100 (2008-11-15)
changeset 28799ee65e7d043fc
parent 28798 a0dd52dd7b55
child 28800 48f7bfebd31d
Thm.proof_of returns proof_body;
src/HOL/Tools/datatype_realizer.ML
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Sat Nov 15 21:31:15 2008 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sat Nov 15 21:31:17 2008 +0100
     1.3 @@ -27,7 +27,8 @@
     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) (Thm.proof_of thm);
     1.8 +  Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm)
     1.9 +    (Proofterm.proof_of (Thm.proof_of thm));
    1.10  
    1.11  fun prf_subst_vars inst =
    1.12    Proofterm.map_proof_terms (subst_vars ([], inst)) I;
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Nov 15 21:31:15 2008 +0100
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Nov 15 21:31:17 2008 +0100
     2.3 @@ -469,7 +469,7 @@
     2.4          let
     2.5            val (ctxt, (_, thm)) = Proof.get_goal state;
     2.6            val thy = ProofContext.theory_of ctxt;
     2.7 -          val prf = Thm.proof_of thm;
     2.8 +          val prf = Proofterm.proof_of (Thm.proof_of thm);
     2.9            val prop = Thm.full_prop_of thm;
    2.10            val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
    2.11          in