# HG changeset patch
# User wenzelm
# Date 1122916829 -7200
# Node ID 34ed8d5d4f16ca2bf1f7f646b81d52a56341d4cd
# Parent  0f8ebabf31639c42df83ea0ed8d880feb13d037e
Sign.read_term;

diff -r 0f8ebabf3163 -r 34ed8d5d4f16 TFL/post.ML
--- 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;
 
diff -r 0f8ebabf3163 -r 34ed8d5d4f16 src/HOL/Tools/inductive_package.ML
--- 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)