src/Pure/Proof/extraction.ML

--- a/src/Pure/Proof/extraction.ML	Fri Sep 26 09:09:53 2008 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Sep 26 09:10:02 2008 +0200
@@ -739,7 +739,7 @@
                       (ProofChecker.thm_of_proof thy'
                        (fst (Proofterm.freeze_thaw_prf prf))))))
              |> snd
-             |> fold Code.add_default_func def_thms
+             |> fold Code.add_default_eqn def_thms
            end
        | SOME _ => thy);