src/Pure/Proof/extraction.ML
changeset 35985 0bbf0d2348f9
parent 35845 e5980f0ad025
child 36042 85efdadee8ae
     1.1 --- a/src/Pure/Proof/extraction.ML	Sat Mar 27 14:10:37 2010 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sat Mar 27 15:20:31 2010 +0100
     1.3 @@ -733,7 +733,7 @@
     1.4               thy'
     1.5               |> PureThy.store_thm (Binding.qualified_name (corr_name s vs),
     1.6                    Thm.varifyT_global (funpow (length (OldTerm.term_vars corr_prop))
     1.7 -                    (Thm.forall_elim_var 0) (forall_intr_frees
     1.8 +                    (Thm.forall_elim_var 0) (Thm.forall_intr_frees
     1.9                        (ProofChecker.thm_of_proof thy'
    1.10                         (fst (Proofterm.freeze_thaw_prf prf))))))
    1.11               |> snd