src/HOL/Tools/inductive_package.ML
changeset 12922 ed70a600f0ea
parent 12902 a23dc0b7566f
child 13197 0567f4fd1415
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Feb 21 20:10:05 2002 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Feb 21 20:10:34 2002 +0100
     1.3 @@ -614,9 +614,12 @@
     1.4  
     1.5      val sign = Theory.sign_of thy;
     1.6  
     1.7 -    val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
     1.8 -        None => []
     1.9 -      | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
    1.10 +    val sum_case_rewrites =
    1.11 +      (if PureThy.get_name thy = "Datatype" then PureThy.get_thms thy "sum.cases"
    1.12 +        else
    1.13 +          (case ThyInfo.lookup_theory "Datatype" of
    1.14 +            None => []
    1.15 +          | Some thy' => PureThy.get_thms thy' "sum.cases")) |> map mk_meta_eq;
    1.16  
    1.17      val (preds, ind_prems, mutual_ind_concl, factors) =
    1.18        mk_indrule cs cTs params intr_ts;