Thm.proof_of returns proof_body;
authorwenzelm
Sat Nov 15 21:31:27 2008 +0100 (2008-11-15)
changeset 288058136e5736808
parent 28804 5d3b1df16353
child 28806 ba0ffe4cfc2b
Thm.proof_of returns proof_body;
adapted PThm;
src/Pure/Proof/extraction.ML
     1.1 --- a/src/Pure/Proof/extraction.ML	Sat Nov 15 21:31:25 2008 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sat Nov 15 21:31:27 2008 +0100
     1.3 @@ -544,8 +544,9 @@
     1.4                (defs3, corr_prf1 % u %% corr_prf2)
     1.5            end
     1.6  
     1.7 -      | corr d defs vs ts Ts hs (prf0 as PThm (name, prf, prop, SOME Ts')) _ _ =
     1.8 +      | corr d defs vs ts Ts hs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
     1.9            let
    1.10 +            val prf = force_proof body;
    1.11              val (vs', tye) = find_inst prop Ts ts vs;
    1.12              val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye;
    1.13              val T = etype_of thy' vs' [] prop;
    1.14 @@ -567,8 +568,9 @@
    1.15                      val corr_prop = Reconstruct.prop_of corr_prf;
    1.16                      val corr_prf' = List.foldr forall_intr_prf
    1.17                        (proof_combt
    1.18 -                         (PThm (corr_name name vs', corr_prf, corr_prop,
    1.19 -                             SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop))
    1.20 +                         (PThm (serial (),
    1.21 +                          ((corr_name name vs', corr_prop, SOME (map TVar (term_tvars corr_prop))),
    1.22 +                            Lazy.value (make_proof_body corr_prf))), vfs_of corr_prop))
    1.23                        (map (get_var_type corr_prop) (vfs_of prop))
    1.24                    in
    1.25                      ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
    1.26 @@ -632,8 +634,9 @@
    1.27                in (defs'', f $ t) end
    1.28            end
    1.29  
    1.30 -      | extr d defs vs ts Ts hs (prf0 as PThm (s, prf, prop, SOME Ts')) =
    1.31 +      | extr d defs vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts'), body))) =
    1.32            let
    1.33 +            val prf = force_proof body;
    1.34              val (vs', tye) = find_inst prop Ts ts vs;
    1.35              val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
    1.36            in
    1.37 @@ -676,8 +679,9 @@
    1.38                      val corr_prop = Reconstruct.prop_of corr_prf';
    1.39                      val corr_prf'' = List.foldr forall_intr_prf
    1.40                        (proof_combt
    1.41 -                        (PThm (corr_name s vs', corr_prf', corr_prop,
    1.42 -                          SOME (map TVar (term_tvars corr_prop))),  vfs_of corr_prop))
    1.43 +                        (PThm (serial (),
    1.44 +                         ((corr_name s vs', corr_prop, SOME (map TVar (term_tvars corr_prop))),
    1.45 +                           Lazy.value (make_proof_body corr_prf'))), vfs_of corr_prop))
    1.46                        (map (get_var_type corr_prop) (vfs_of prop));
    1.47                    in
    1.48                      ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
    1.49 @@ -709,7 +713,7 @@
    1.50        let
    1.51          val thy = Thm.theory_of_thm thm;
    1.52          val prop = Thm.prop_of thm;
    1.53 -        val prf = Thm.proof_of thm;
    1.54 +        val prf = proof_of (Thm.proof_of thm);
    1.55          val name = Thm.get_name thm;
    1.56          val _ = name <> "" orelse error "extraction: unnamed theorem";
    1.57          val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^