--- a/src/HOL/Tools/inductive_package.ML Mon Aug 01 19:20:28 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML Mon Aug 01 19:20:29 2005 +0200
@@ -614,7 +614,10 @@
else
(case ThyInfo.lookup_theory "Datatype" of
NONE => []
- | SOME thy' => PureThy.get_thms thy' (Name "sum.cases")))
+ | SOME thy' =>
+ if Theory.subthy (thy', thy) then
+ PureThy.get_thms thy' (Name "sum.cases")
+ else []))
|> map mk_meta_eq;
val (preds, ind_prems, mutual_ind_concl, factors) =
@@ -845,7 +848,7 @@
fun add_inductive verbose coind c_strings intro_srcs raw_monos thy =
let
- val cs = map (term_of o HOLogic.read_cterm thy) c_strings;
+ val cs = map (Sign.read_term thy) c_strings;
val intr_names = map (fst o fst) intro_srcs;
fun read_rule s = Thm.read_cterm thy (s, propT)