# HG changeset patch # User krauss # Date 1293655964 -3600 # Node ID b6dc60638be05dae7a49202e6c77b54e4f5877e1 # Parent 211dbd42f95dc2c5d9a43b1d9a392d66eb738671 more robust decomposition of simultaneous goals diff -r 211dbd42f95d -r b6dc60638be0 src/HOL/Tools/Function/induction_schema.ML --- a/src/HOL/Tools/Function/induction_schema.ML Wed Dec 29 21:52:41 2010 +0100 +++ b/src/HOL/Tools/Function/induction_schema.ML Wed Dec 29 21:52:44 2010 +0100 @@ -71,7 +71,7 @@ end val (branches, cases') = (* correction *) - case Logic.dest_conjunction_list concl of + case Logic.dest_conjunctions concl of [conc] => let val _ $ Pxs = Logic.strip_assums_concl conc