src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 57038 2114f3224b2c
parent 56858 0c3d0bc98abe
child 57090 0224caba67ca
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed May 21 14:09:42 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed May 21 14:09:42 2014 +0200
     1.3 @@ -932,8 +932,11 @@
     1.4             (flat nontriv_disc_eq_thmss, code_nitpicksimp_attrs)]
     1.5            |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
     1.6  
     1.7 +        (* "exhaust" is deliberately put first to avoid apparent circular dependencies in the proof
     1.8 +           objects, which would confuse MaSh. *)
     1.9          val notes =
    1.10 -          [(caseN, case_thms, code_nitpicksimp_simp_attrs),
    1.11 +          [(exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
    1.12 +           (caseN, case_thms, code_nitpicksimp_simp_attrs),
    1.13             (case_congN, [case_cong_thm], []),
    1.14             (case_eq_ifN, case_eq_if_thms, []),
    1.15             (collapseN, safe_collapse_thms, simp_attrs),
    1.16 @@ -942,7 +945,6 @@
    1.17             (disc_excludeN, disc_exclude_thms, dest_attrs),
    1.18             (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
    1.19             (distinctN, distinct_thms, simp_attrs @ inductsimp_attrs),
    1.20 -           (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
    1.21             (expandN, expand_thms, []),
    1.22             (injectN, inject_thms, iff_attrs @ inductsimp_attrs),
    1.23             (nchotomyN, [nchotomy_thm], []),