merged

--- 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