# HG changeset patch
# User wenzelm
# Date 955576370 -7200
# Node ID 88dafea5955c43e13e48b17805bee41a78fe4bf9
# Parent  37cbb053791cc405acebc0558737357b327ae371
InductMethod.concls_of;

diff -r 37cbb053791c -r 88dafea5955c src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Apr 12 23:52:21 2000 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Wed Apr 12 23:52:50 2000 +0200
@@ -192,8 +192,8 @@
           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 = HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of rule));
-    val insts = flat (map2 prep_inst (concls, varss)) handle LIST _ =>
+    val concls = InductMethod.concls_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;