# HG changeset patch
# User Andreas Lochbihler
# Date 1530305794 -7200
# Node ID bbc7423581564c5dae7dab76540860803b1a9823
# Parent  549a4992222f71f7cf7f8777cd50199ae5cadfca
declare case theorems as proper code equations

diff -r 549a4992222f -r bbc742358156 src/HOL/Library/code_lazy.ML
--- a/src/HOL/Library/code_lazy.ML	Fri Jun 29 22:14:33 2018 +0200
+++ b/src/HOL/Library/code_lazy.ML	Fri Jun 29 22:56:34 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