src/Pure/Proof/extraction.ML
changeset 63239 d562c9948dee
parent 62958 b41c1cb5e251
child 64556 851ae0e7b09c
     1.1 --- a/src/Pure/Proof/extraction.ML	Mon Jun 06 21:28:45 2016 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Mon Jun 06 21:28:46 2016 +0200
     1.3 @@ -810,7 +810,7 @@
     1.4                        (Proof_Checker.thm_of_proof thy'
     1.5                         (fst (Proofterm.freeze_thaw_prf prf))))))
     1.6               |> snd
     1.7 -             |> fold Code.add_default_eqn def_thms
     1.8 +             |> fold (Code.add_eqn (Code.Equation, true)) def_thms
     1.9             end
    1.10         | SOME _ => thy);
    1.11