diff -r 9ab014d47c4d -r 533dd8cda12c src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Sep 29 11:36:16 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Sep 29 11:55:08 2010 +0200
@@ -178,17 +178,6 @@
               |> maps (fn (res, (names, prems)) =>
                 flatten' (betapply (g, res)) (names, prems))
             end)
-        | Const (@{const_name prod_case}, _) => 
-            (let
-              val (_, g :: res :: args) = strip_comb t
-              val [res1, res2] = Name.variant_list names ["res1", "res2"]
-              val (T1, T2) = HOLogic.dest_prodT (fastype_of res)
-              val (resv1, resv2) = (Free (res1, T1), Free (res2, T2))
-            in
-              flatten' (betapplys (g, (resv1 :: resv2 :: args)))
-              (res1 :: res2 :: names,
-              HOLogic.mk_Trueprop (HOLogic.mk_eq (res, HOLogic.mk_prod (resv1, resv2))) :: prems)
-            end)
         | _ =>
         case find_split_thm thy (fst (strip_comb t)) of
           SOME raw_split_thm =>