Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
InductMethod.concls_of;
authorwenzelm
Wed, 12 Apr 2000 23:52:50 +0200
changeset 8697 88dafea5955c
parent 8696 37cbb053791c
child 8698 8812dad6ef12
InductMethod.concls_of;
src/HOL/Tools/datatype_package.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle