changeset 41418 | b6dc60638be0 |
parent 41228 | e1fce873b814 |
child 42361 | 23f352990944 |
--- 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