1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Wed Dec 29 21:52:41 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Wed Dec 29 21:52:44 2010 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4        end
     1.5  
     1.6      val (branches, cases') = (* correction *)
     1.7 -      case Logic.dest_conjunction_list concl of
     1.8 +      case Logic.dest_conjunctions concl of
     1.9          [conc] =>
    1.10          let
    1.11            val _ $ Pxs = Logic.strip_assums_concl conc