src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML

             in
               flatten' f (names, prems)
               |> maps (fn (res, (names, prems)) =>
                 flatten' (betapply (g, res)) (names, prems))
             end)
-        | Const (@{const_name "split"}, _) => 
+        | Const (@{const_name split}, _) => 
             (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))