src/HOL/Tools/inductive_package.ML
changeset 15463 95cb3eb74307
parent 15416 db69af736ebb
child 15525 396268ad58b3
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Jan 24 18:15:19 2005 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Jan 24 18:16:57 2005 +0100
     1.3 @@ -51,7 +51,7 @@
     1.4        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
     1.5         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
     1.6    val add_inductive: bool -> bool -> string list ->
     1.7 -    ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
     1.8 +    ((bstring * string) * Args.src list) list -> (thmref * Args.src list) list ->
     1.9      theory -> theory *
    1.10        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    1.11         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    1.12 @@ -617,11 +617,11 @@
    1.13      val sign = Theory.sign_of thy;
    1.14  
    1.15      val sum_case_rewrites =
    1.16 -      (if PureThy.get_name thy = "Datatype" then PureThy.get_thms thy "sum.cases"
    1.17 +      (if PureThy.get_name thy = "Datatype" then PureThy.get_thms thy ("sum.cases", None)
    1.18          else
    1.19            (case ThyInfo.lookup_theory "Datatype" of
    1.20              None => []
    1.21 -          | Some thy' => PureThy.get_thms thy' "sum.cases")) |> map mk_meta_eq;
    1.22 +          | Some thy' => PureThy.get_thms thy' ("sum.cases", None))) |> map mk_meta_eq;
    1.23  
    1.24      val (preds, ind_prems, mutual_ind_concl, factors) =
    1.25        mk_indrule cs cTs params intr_ts;