src/HOL/Tools/inductive_package.ML

   let
     val _ = message "  Proving the induction rule ...";
 
     val sign = Theory.sign_of thy;
 
+    val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
+        None => []
+      | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
+
     val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
 
     (* make predicate for instantiation of abstract induction rule *)
 
     fun mk_ind_pred _ [P] = P
       | mk_ind_pred T Ps =
          let val n = (length Ps) div 2;
              val Type (_, [T1, T2]) = T
-         in Const ("basic_sum_case",
+         in Const ("Datatype.sum.sum_case",
            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
              mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
          end;
 
     val ind_pred = mk_ind_pred sumT preds;

       map (fn c => prove_goalw_cterm [] (cterm_of sign
         (HOLogic.mk_Trueprop (HOLogic.mk_eq
           (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
              nth_elem (find_index_eq c cs, preds)))))
-        (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac
-           (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
+        (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites,
           rtac refl 1])) cs;
 
     val induct = prove_goalw_cterm [] (cterm_of sign
       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
         [rtac (impI RS allI) 1,

          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
          (*Now break down the individual cases.  No disjE here in case
            some premise involves disjunction.*)
          REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE] 
                      ORELSE' hyp_subst_tac)),
-         rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
+         rewrite_goals_tac sum_case_rewrites,
          EVERY (map (fn prem =>
            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
 
     val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign
       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
         [cut_facts_tac prems 1,
          REPEAT (EVERY
            [REPEAT (resolve_tac [conjI, impI] 1),
             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
-            rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
+            rewrite_goals_tac sum_case_rewrites,
             atac 1])])
 
   in standard (split_rule (induct RS lemma))
   end;