src/HOL/Tools/inductive_package.ML
changeset 16486 1a12cdb6ee6b
parent 16432 a6e8fb94a8ca
child 16785 2eddcce4fd16
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Jun 20 22:13:58 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Jun 20 22:13:59 2005 +0200
     1.3 @@ -614,11 +614,11 @@
     1.4  
     1.5      val sum_case_rewrites =
     1.6        (if Context.theory_name thy = "Datatype" then
     1.7 -        PureThy.get_thms thy ("sum.cases", NONE)
     1.8 +        PureThy.get_thms thy (Name "sum.cases")
     1.9        else
    1.10          (case ThyInfo.lookup_theory "Datatype" of
    1.11            NONE => []
    1.12 -        | SOME thy' => PureThy.get_thms thy' ("sum.cases", NONE)))
    1.13 +        | SOME thy' => PureThy.get_thms thy' (Name "sum.cases")))
    1.14        |> map mk_meta_eq;
    1.15  
    1.16      val (preds, ind_prems, mutual_ind_concl, factors) =