changeset 24219 | e558fe311376 |
parent 23178 | 07ba6b58b3d2 |
child 24624 | b8383b1bbae3 |
--- a/src/Pure/Proof/extraction.ML Fri Aug 10 17:04:24 2007 +0200 +++ b/src/Pure/Proof/extraction.ML Fri Aug 10 17:04:34 2007 +0200 @@ -741,7 +741,7 @@ (ProofChecker.thm_of_proof thy' (fst (Proofterm.freeze_thaw_prf prf)))))), []) |> snd - |> fold (CodegenData.add_func false) def_thms + |> fold (Code.add_func false) def_thms end | SOME _ => thy);