# HG changeset patch
# User haftmann
# Date 1177060913 -7200
# Node ID bff5d59de79bd9f4ece10c1690d3fc7abfd413ab
# Parent  189efc4a9f541f4048b209edad0b3bc1a7efc9de
adds extracted program to code theorem table

diff -r 189efc4a9f54 -r bff5d59de79b src/Pure/Proof/extraction.ML
--- 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);