equal
deleted
inserted
replaced
622 val corr_prf = mkabsp shyps corr_prf0; |
622 val corr_prf = mkabsp shyps corr_prf0; |
623 val corr_prop = Proofterm.prop_of corr_prf; |
623 val corr_prop = Proofterm.prop_of corr_prf; |
624 val corr_header = |
624 val corr_header = |
625 Proofterm.thm_header (Proofterm.proof_serial ()) pos (corr_name name vs') |
625 Proofterm.thm_header (Proofterm.proof_serial ()) pos (corr_name name vs') |
626 corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev))); |
626 corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev))); |
627 val corr_body = |
627 val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf); |
628 Proofterm.thm_body I (Future.value (Proofterm.approximate_proof_body corr_prf)); |
|
629 val corr_prf' = |
628 val corr_prf' = |
630 Proofterm.proof_combP |
629 Proofterm.proof_combP |
631 (Proofterm.proof_combt |
630 (Proofterm.proof_combt |
632 (PThm (corr_header, corr_body), vfs_of corr_prop), |
631 (PThm (corr_header, corr_body), vfs_of corr_prop), |
633 map PBound (length shyps - 1 downto 0)) |> |
632 map PBound (length shyps - 1 downto 0)) |> |
743 SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf); |
742 SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf); |
744 val corr_prop = Proofterm.prop_of corr_prf'; |
743 val corr_prop = Proofterm.prop_of corr_prf'; |
745 val corr_header = |
744 val corr_header = |
746 Proofterm.thm_header (Proofterm.proof_serial ()) pos (corr_name s vs') |
745 Proofterm.thm_header (Proofterm.proof_serial ()) pos (corr_name s vs') |
747 corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev))); |
746 corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev))); |
748 val corr_body = |
747 val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf'); |
749 Proofterm.thm_body I |
|
750 (Future.value (Proofterm.approximate_proof_body corr_prf')); |
|
751 val corr_prf'' = |
748 val corr_prf'' = |
752 Proofterm.proof_combP (Proofterm.proof_combt |
749 Proofterm.proof_combP (Proofterm.proof_combt |
753 (PThm (corr_header, corr_body), vfs_of corr_prop), |
750 (PThm (corr_header, corr_body), vfs_of corr_prop), |
754 map PBound (length shyps - 1 downto 0)) |> |
751 map PBound (length shyps - 1 downto 0)) |> |
755 fold_rev Proofterm.forall_intr_proof' |
752 fold_rev Proofterm.forall_intr_proof' |