# HG changeset patch
# User wenzelm
# Date 1175722178 -7200
# Node ID f31a869077f0b405c5a0d2c35d59e5e4650645b9
# Parent  284b2183d070ff780229eaff952c413c5f42ac8b
rep_thm/cterm/ctyp: removed obsolete sign field;
renamed Variable.importT to importT_thms;

diff -r 284b2183d070 -r f31a869077f0 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Apr 04 23:29:37 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Wed Apr 04 23:29:38 2007 +0200
@@ -195,8 +195,8 @@
           SOME r => (r, "Induction rule")
         | NONE =>
             let val tn = find_tname (hd (map_filter I (flat varss))) Bi
-                val {sign, ...} = Thm.rep_thm state
-            in (#induction (the_datatype sign tn), "Induction rule for type " ^ tn) 
+                val thy = Thm.theory_of_thm state
+            in (#induction (the_datatype thy tn), "Induction rule for type " ^ tn) 
             end
     val concls = HOLogic.dest_concls (Thm.concl_of rule);
     val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
@@ -825,7 +825,8 @@
       ||>> fold_map apply_theorems raw_inject
       ||>> apply_theorems [raw_induction];
 
-    val ((_, [induction']), _) = Variable.importT [induction] (Variable.thm_context induction);
+    val ((_, [induction']), _) =
+      Variable.importT_thms [induction] (Variable.thm_context induction);
 
     fun err t = error ("Ill-formed predicate in induction rule: " ^
       Sign.string_of_term thy1 t);