diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -2608,7 +2608,7 @@
 section \<open>First implementation : Naive by encoding all case splits locally\<close>
 
 definition "msubsteq c t d s a r =
-  evaldjf (split conj)
+  evaldjf (case_prod conj)
   [(let cd = c *\<^sub>p d
     in (NEq (CP cd), Eq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
    (conj (Eq (CP c)) (NEq (CP d)), Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
@@ -2626,7 +2626,7 @@
       in (NEq (CP cd), Eq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
      (conj (Eq (CP c)) (NEq (CP d)), Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
      (conj (NEq (CP c)) (Eq (CP d)), Eq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
-     (conj (Eq (CP c)) (Eq (CP d)), Eq r)]. bound0 (split conj x)"
+     (conj (Eq (CP c)) (Eq (CP d)), Eq r)]. bound0 (case_prod conj x)"
     using lp by (simp add: Let_def t s)
   from evaldjf_bound0[OF th] show ?thesis
     by (simp add: msubsteq_def)
@@ -2715,7 +2715,7 @@
 
 
 definition "msubstneq c t d s a r =
-  evaldjf (split conj)
+  evaldjf (case_prod conj)
   [(let cd = c *\<^sub>p d
     in (NEq (CP cd), NEq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
    (conj (Eq (CP c)) (NEq (CP d)), NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
@@ -2733,7 +2733,7 @@
      in (NEq (CP cd), NEq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
     (conj (Eq (CP c)) (NEq (CP d)), NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
     (conj (NEq (CP c)) (Eq (CP d)), NEq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
-    (conj (Eq (CP c)) (Eq (CP d)), NEq r)]. bound0 (split conj x)"
+    (conj (Eq (CP c)) (Eq (CP d)), NEq r)]. bound0 (case_prod conj x)"
     using lp by (simp add: Let_def t s)
   from evaldjf_bound0[OF th] show ?thesis
     by (simp add: msubstneq_def)
@@ -2821,7 +2821,7 @@
 qed
 
 definition "msubstlt c t d s a r =
-  evaldjf (split conj)
+  evaldjf (case_prod conj)
   [(let cd = c *\<^sub>p d
     in (lt (CP (~\<^sub>p cd)), Lt (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
    (let cd = c *\<^sub>p d
@@ -2847,7 +2847,7 @@
    (conj (lt (CP c)) (Eq (CP d)), Lt (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
    (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)), Lt (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
    (conj (lt (CP d)) (Eq (CP c)), Lt (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
-   (conj (Eq (CP c)) (Eq (CP d)), Lt r)]. bound0 (split conj x)"
+   (conj (Eq (CP c)) (Eq (CP d)), Lt r)]. bound0 (case_prod conj x)"
     using lp by (simp add: Let_def t s lt_nb)
   from evaldjf_bound0[OF th] show ?thesis
     by (simp add: msubstlt_def)
@@ -3027,7 +3027,7 @@
 qed
 
 definition "msubstle c t d s a r =
-  evaldjf (split conj)
+  evaldjf (case_prod conj)
    [(let cd = c *\<^sub>p d
      in (lt (CP (~\<^sub>p cd)), Le (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
     (let cd = c *\<^sub>p d
@@ -3053,7 +3053,7 @@
     (conj (lt (CP c)) (Eq (CP d)) , Le (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
     (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Le (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
     (conj (lt (CP d)) (Eq (CP c)) , Le (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
-    (conj (Eq (CP c)) (Eq (CP d)) , Le r)]. bound0 (split conj x)"
+    (conj (Eq (CP c)) (Eq (CP d)) , Le r)]. bound0 (case_prod conj x)"
     using lp by (simp add: Let_def t s lt_nb)
   from evaldjf_bound0[OF th] show ?thesis
     by (simp add: msubstle_def)