author haftmann Fri, 20 Apr 2007 11:21:53 +0200 changeset 22750 bff5d59de79b parent 22749 189efc4a9f54 child 22751 1bfd75c1f232
adds extracted program to code theorem table
```--- a/src/Pure/Proof/extraction.ML	Fri Apr 20 11:21:52 2007 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Apr 20 11:21:53 2007 +0200
@@ -578,7 +578,7 @@
(proof_combt
(PThm (corr_name name vs', corr_prf, corr_prop,
SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop))
-		      (map (get_var_type corr_prop) (vfs_of prop))
+                      (map (get_var_type corr_prop) (vfs_of prop))
in
((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
prf_subst_TVars tye' corr_prf')
@@ -687,7 +687,7 @@
(proof_combt
(PThm (corr_name s vs', corr_prf', corr_prop,
SOME (map TVar (term_tvars corr_prop))),  vfs_of corr_prop))
-		      (map (get_var_type corr_prop) (vfs_of prop));
+                      (map (get_var_type corr_prop) (vfs_of prop));
in
((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
subst_TVars tye' u)
@@ -733,16 +733,20 @@
val corr_prop = Reconstruct.prop_of prf;
val ft = Type.freeze t;
val fu = Type.freeze u;
-             val thy' = if t = nullt then thy else thy |>
-               Theory.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)] |>
-               snd o PureThy.add_defs_i false [((extr_name s vs ^ "_def",
-                 Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])];
+             val (def_thms, thy') = if t = nullt then ([], thy) else
+               thy
+               |> Theory.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)]
+               |> PureThy.add_defs_i false [((extr_name s vs ^ "_def",
+                    Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
in
-             snd (PureThy.store_thm ((corr_name s vs,
-               Thm.varifyT (funpow (length (term_vars corr_prop))
-                 (forall_elim_var 0) (forall_intr_frees
-                   (ProofChecker.thm_of_proof thy'
-                     (fst (Proofterm.freeze_thaw_prf prf)))))), []) thy')
+             thy'
+             |> PureThy.store_thm ((corr_name s vs,
+                  Thm.varifyT (funpow (length (term_vars corr_prop))
+                    (forall_elim_var 0) (forall_intr_frees
+                      (ProofChecker.thm_of_proof thy'
+                       (fst (Proofterm.freeze_thaw_prf prf)))))), [])
+             |> snd
+             |> fold (CodegenData.add_func false) def_thms
end
| SOME _ => thy);
```