rep_thm/cterm/ctyp: removed obsolete sign field;
renamed Variable.importT to importT_thms;

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