# HG changeset patch
# User Andreas Lochbihler
# Date 1530306276 -7200
# Node ID 516e81f7595742c86bbdaebf41bef3bc8ded3a15
# Parent  a22540ac70528dfc8c1b1cb7f2fb88d1b2d69d7b# Parent  bbc7423581564c5dae7dab76540860803b1a9823
merged

diff -r a22540ac7052 -r 516e81f75957 src/HOL/Library/code_lazy.ML
--- a/src/HOL/Library/code_lazy.ML	Fri Jun 29 22:50:35 2018 +0200
+++ b/src/HOL/Library/code_lazy.ML	Fri Jun 29 23:04:36 2018 +0200
@@ -487,9 +487,9 @@
     val add_lazy_ctr_thms = fold (Code.add_eqn_global o rpair true) ctrs_lazy_thms
     val add_lazy_case_thms =
       fold Code.del_eqn_global case_thms
-      #> Code.add_eqn_global (case_lazy_thm, false)
+      #> Code.add_eqn_global (case_lazy_thm, true)
     val add_eager_case_thms = Code.del_eqn_global case_lazy_thm
-      #> fold (Code.add_eqn_global o rpair false) case_thms
+      #> fold (Code.add_eqn_global o rpair true) case_thms
 
     val delay_dummy_thm = (pat_def_thm RS @{thm symmetric})
       |> Drule.infer_instantiate' lthy10