Sign.read_term;

--- a/TFL/post.ML	Mon Aug 01 19:20:28 2005 +0200
+++ b/TFL/post.ML	Mon Aug 01 19:20:29 2005 +0200
@@ -37,9 +37,6 @@
 
 (* misc *)
 
-val read_term = Thm.term_of oo (HOLogic.read_cterm o Theory.sign_of);
-
-
 (*---------------------------------------------------------------------------
  * Extract termination goals so that they can be put it into a goalstack, or
  * have a tactic directly applied to them.
@@ -248,7 +245,7 @@
   in (thy, {rules = rules', induct = induct, tcs = tcs}) end;
 
 fun define strict thy cs ss congs wfs fid R seqs =
-  define_i strict thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs)
+  define_i strict thy cs ss congs wfs fid (Sign.read_term thy R) (map (Sign.read_term thy) seqs)
     handle U.ERR {mesg,...} => error mesg;
 
 
@@ -275,7 +272,7 @@
  end
 
 fun defer thy congs fid seqs =
-  defer_i thy congs fid (map (read_term thy) seqs)
+  defer_i thy congs fid (map (Sign.read_term thy) seqs)
     handle U.ERR {mesg,...} => error mesg;
 end;
 

--- 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)