
diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Induct/Com.thy
--- a/src/HOL/Induct/Com.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Induct/Com.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -139,7 +139,7 @@
 text\<open>Make the induction rule look nicer -- though @{text eta_contract} makes the new
     version look worse than it is...\<close>
 
-lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
+lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (case_prod (%v. case_prod (case_prod P v)))"
   by auto
 
 text\<open>New induction rule.  Note the form of the VALOF induction hypothesis\<close>




