# 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