src/Pure/Proof/extraction.ML
changeset 28370 37f56e6e702d
parent 27865 27a8ad9612a3
child 28375 c879d88d038a
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Sep 26 09:09:53 2008 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Sep 26 09:10:02 2008 +0200
     1.3 @@ -739,7 +739,7 @@
     1.4                        (ProofChecker.thm_of_proof thy'
     1.5                         (fst (Proofterm.freeze_thaw_prf prf))))))
     1.6               |> snd
     1.7 -             |> fold Code.add_default_func def_thms
     1.8 +             |> fold Code.add_default_eqn def_thms
     1.9             end
    1.10         | SOME _ => thy);
    1.11