--- a/src/HOL/Tools/inductive_package.ML Thu Feb 21 20:10:05 2002 +0100
+++ b/src/HOL/Tools/inductive_package.ML Thu Feb 21 20:10:34 2002 +0100
@@ -614,9 +614,12 @@
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 sum_case_rewrites =
+ (if PureThy.get_name thy = "Datatype" then PureThy.get_thms thy "sum.cases"
+ else
+ (case ThyInfo.lookup_theory "Datatype" of
+ None => []
+ | Some thy' => PureThy.get_thms thy' "sum.cases")) |> map mk_meta_eq;
val (preds, ind_prems, mutual_ind_concl, factors) =
mk_indrule cs cTs params intr_ts;