# HG changeset patch
# User blanchet
# Date 1400674182 -7200
# Node ID 2114f3224b2cd17f46398796f9bac4d886507c2a
# Parent  c51132be8e1633b4bb34fcc8676dcc33a240fa4e
move exhaust first, for technical reasons

diff -r c51132be8e16 -r 2114f3224b2c src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed May 21 14:09:42 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed May 21 14:09:42 2014 +0200
@@ -932,8 +932,11 @@
            (flat nontriv_disc_eq_thmss, code_nitpicksimp_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 
+        (* "exhaust" is deliberately put first to avoid apparent circular dependencies in the proof
+           objects, which would confuse MaSh. *)
         val notes =
-          [(caseN, case_thms, code_nitpicksimp_simp_attrs),
+          [(exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
+           (caseN, case_thms, code_nitpicksimp_simp_attrs),
            (case_congN, [case_cong_thm], []),
            (case_eq_ifN, case_eq_if_thms, []),
            (collapseN, safe_collapse_thms, simp_attrs),
@@ -942,7 +945,6 @@
            (disc_excludeN, disc_exclude_thms, dest_attrs),
            (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
            (distinctN, distinct_thms, simp_attrs @ inductsimp_attrs),
-           (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
            (expandN, expand_thms, []),
            (injectN, inject_thms, iff_attrs @ inductsimp_attrs),
            (nchotomyN, [nchotomy_thm], []),