# 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