# HG changeset patch
# User wenzelm
# Date 1002881170 -7200
# Node ID d0c37d04906b65ffca256e34e33c9450e3dc0732
# Parent  f727aa96ae2ee2b813c336bd48a0530f0d01a21d
HOLogic.dest_concls, InductAttrib.vars_of;

diff -r f727aa96ae2e -r d0c37d04906b src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Fri Oct 12 12:05:46 2001 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Fri Oct 12 12:06:10 2001 +0200
@@ -183,7 +183,7 @@
   | prep_var _ = None;
 
 fun prep_inst (concl, xs) =	(*exception LIST*)
-  let val vs = InductMethod.vars_of concl
+  let val vs = InductAttrib.vars_of concl
   in mapfilter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
 
 in
@@ -199,7 +199,7 @@
           let val tn = find_tname (hd (mapfilter I (flat varss))) Bi
           in (#induction (datatype_info_sg_err sign tn), "Induction rule for type " ^ tn) end);
 
-    val concls = InductMethod.concls_of rule;
+    val concls = HOLogic.dest_concls (Thm.concl_of rule);
     val insts = flat (map prep_inst (concls ~~ varss)) handle LIST _ =>
       error (rule_name ^ " has different numbers of variables");
   in occs_in_prems (Tactic.res_inst_tac insts rule) (map #2 insts) i state end;