src/HOL/Tools/inductive_package.ML
changeset 16975 34ed8d5d4f16
parent 16934 9ef19e3c7fdd
child 17010 5abc26872268
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Aug 01 19:20:28 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Aug 01 19:20:29 2005 +0200
     1.3 @@ -614,7 +614,10 @@
     1.4        else
     1.5          (case ThyInfo.lookup_theory "Datatype" of
     1.6            NONE => []
     1.7 -        | SOME thy' => PureThy.get_thms thy' (Name "sum.cases")))
     1.8 +        | SOME thy' =>
     1.9 +            if Theory.subthy (thy', thy) then
    1.10 +              PureThy.get_thms thy' (Name "sum.cases")
    1.11 +            else []))
    1.12        |> map mk_meta_eq;
    1.13  
    1.14      val (preds, ind_prems, mutual_ind_concl, factors) =
    1.15 @@ -845,7 +848,7 @@
    1.16  
    1.17  fun add_inductive verbose coind c_strings intro_srcs raw_monos thy =
    1.18    let
    1.19 -    val cs = map (term_of o HOLogic.read_cterm thy) c_strings;
    1.20 +    val cs = map (Sign.read_term thy) c_strings;
    1.21  
    1.22      val intr_names = map (fst o fst) intro_srcs;
    1.23      fun read_rule s = Thm.read_cterm thy (s, propT)