src/HOL/Tools/datatype_realizer.ML
changeset 28799 ee65e7d043fc
parent 26626 c6231d64d264
child 28814 463c9e9111ae
equal deleted inserted replaced
28798:a0dd52dd7b55 28799:ee65e7d043fc
    25 fun forall_intr_prf (t, prf) =
    25 fun forall_intr_prf (t, prf) =
    26   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    26   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    27   in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
    27   in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
    28 
    28 
    29 fun prf_of thm =
    29 fun prf_of thm =
    30   Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
    30   Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm)
       
    31     (Proofterm.proof_of (Thm.proof_of thm));
    31 
    32 
    32 fun prf_subst_vars inst =
    33 fun prf_subst_vars inst =
    33   Proofterm.map_proof_terms (subst_vars ([], inst)) I;
    34   Proofterm.map_proof_terms (subst_vars ([], inst)) I;
    34 
    35 
    35 fun is_unit t = snd (strip_type (fastype_of t)) = HOLogic.unitT;
    36 fun is_unit t = snd (strip_type (fastype_of t)) = HOLogic.unitT;