1.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -16,23 +16,23 @@
     1.4  
     1.5  subsection {* Curry in a Hurry *}
     1.6  
     1.7 -lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
     1.8 +lemma "(\<lambda>f x y. (curry o case_prod) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
     1.9  nitpick [card = 1-12, expect = none]
    1.10  by auto
    1.11  
    1.12 -lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
    1.13 +lemma "(\<lambda>f p. (case_prod o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
    1.14  nitpick [card = 1-12, expect = none]
    1.15  by auto
    1.16  
    1.17 -lemma "split (curry f) = f"
    1.18 +lemma "case_prod (curry f) = f"
    1.19  nitpick [card = 1-12, expect = none]
    1.20  by auto
    1.21  
    1.22 -lemma "curry (split f) = f"
    1.23 +lemma "curry (case_prod f) = f"
    1.24  nitpick [card = 1-12, expect = none]
    1.25  by auto
    1.26  
    1.27 -lemma "split (\<lambda>x y. f (x, y)) = f"
    1.28 +lemma "case_prod (\<lambda>x y. f (x, y)) = f"
    1.29  nitpick [card = 1-12, expect = none]
    1.30  by auto
    1.31  
    1.32 @@ -139,7 +139,7 @@
    1.33  nitpick [card = 2, expect = none]
    1.34  by auto
    1.35  
    1.36 -lemma "f = split"
    1.37 +lemma "f = case_prod"
    1.38  nitpick [card = 2, expect = genuine]
    1.39  oops
    1.40