src/Pure/Proof/extraction.ML

                   Thm.varifyT_global (funpow (length (vars_of corr_prop))
                     (Thm.forall_elim_var 0) (Thm.forall_intr_frees
                       (Proof_Checker.thm_of_proof thy'
                        (fst (Proofterm.freeze_thaw_prf prf))))))
              |> snd
-             |> fold Code.add_default_eqn def_thms
+             |> fold (Code.add_eqn (Code.Equation, true)) def_thms
            end
        | SOME _ => thy);
 
   in
     thy