changeset 26653 | 60e0cf6bef89 |
parent 26626 | c6231d64d264 |
child 26939 | 1035c89b4c02 |
--- a/src/Pure/Proof/extraction.ML Tue Apr 15 16:12:01 2008 +0200 +++ b/src/Pure/Proof/extraction.ML Tue Apr 15 16:12:05 2008 +0200 @@ -739,7 +739,7 @@ thy' |> PureThy.store_thm (corr_name s vs, Thm.varifyT (funpow (length (term_vars corr_prop)) - (forall_elim_var 0) (forall_intr_frees + (Thm.forall_elim_var 0) (forall_intr_frees (ProofChecker.thm_of_proof thy' (fst (Proofterm.freeze_thaw_prf prf)))))) |> snd