# HG changeset patch
# User wenzelm
# Date 933609480 -7200
# Node ID de17299bf09586582d1256376edc9ee11f099b6f
# Parent  d203e2282789567f6b8614b22a7a36b8b96b8cf0
handle LIST _;

diff -r d203e2282789 -r de17299bf095 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Aug 02 15:40:30 1999 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Mon Aug 02 17:58:00 1999 +0200
@@ -179,7 +179,7 @@
     val ind_vnames = map (fn (_ $ Var (ixn, _)) =>
       implode (tl (explode (Syntax.string_of_vname ixn))))
         (dest_conj (HOLogic.dest_Trueprop (concl_of induction)));
-    val insts = (ind_vnames ~~ vars) handle _ =>
+    val insts = (ind_vnames ~~ vars) handle LIST _ =>
       error ("Induction rule for type " ^ tn ^ " has different number of variables")
   in
     occs_in_prems (res_inst_tac insts induction) vars i state