src/HOL/Library/code_lazy.ML
changeset 68549 bbc742358156
parent 68155 8b50f29a1992
child 69568 de09a7261120
     1.1 --- a/src/HOL/Library/code_lazy.ML	Fri Jun 29 22:14:33 2018 +0200
     1.2 +++ b/src/HOL/Library/code_lazy.ML	Fri Jun 29 22:56:34 2018 +0200
     1.3 @@ -487,9 +487,9 @@
     1.4      val add_lazy_ctr_thms = fold (Code.add_eqn_global o rpair true) ctrs_lazy_thms
     1.5      val add_lazy_case_thms =
     1.6        fold Code.del_eqn_global case_thms
     1.7 -      #> Code.add_eqn_global (case_lazy_thm, false)
     1.8 +      #> Code.add_eqn_global (case_lazy_thm, true)
     1.9      val add_eager_case_thms = Code.del_eqn_global case_lazy_thm
    1.10 -      #> fold (Code.add_eqn_global o rpair false) case_thms
    1.11 +      #> fold (Code.add_eqn_global o rpair true) case_thms
    1.12  
    1.13      val delay_dummy_thm = (pat_def_thm RS @{thm symmetric})
    1.14        |> Drule.infer_instantiate' lthy10