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.
handle LIST _;
authorwenzelm
Mon, 02 Aug 1999 17:58:00 +0200
changeset 7151 de17299bf095
parent 7150 d203e2282789
child 7152 44d46a112127
handle LIST _;
src/HOL/Tools/datatype_package.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle