src/Pure/Proof/extraction.ML
changeset 26481 92e901171cc8
parent 26463 9283b4185fdf
child 26626 c6231d64d264
     1.1 --- a/src/Pure/Proof/extraction.ML	Sat Mar 29 19:14:00 2008 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sat Mar 29 19:14:03 2008 +0100
     1.3 @@ -735,11 +735,11 @@
     1.4                      Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
     1.5             in
     1.6               thy'
     1.7 -             |> PureThy.store_thm ((corr_name s vs,
     1.8 +             |> PureThy.store_thm (corr_name s vs,
     1.9                    Thm.varifyT (funpow (length (term_vars corr_prop))
    1.10                      (forall_elim_var 0) (forall_intr_frees
    1.11                        (ProofChecker.thm_of_proof thy'
    1.12 -                       (fst (Proofterm.freeze_thaw_prf prf)))))), [])
    1.13 +                       (fst (Proofterm.freeze_thaw_prf prf))))))
    1.14               |> snd
    1.15               |> fold Code.add_default_func def_thms
    1.16             end