src/HOL/Tools/Predicate_Compile/code_prolog.ML

     val options = code_options_of (Proof_Context.theory_of ctxt)
     val split =
       (case t_compr of
         (Const (@{const_name Collect}, _) $ t) => t
       | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr))
-    val (body, Ts, fp) = HOLogic.strip_psplits split
+    val (body, Ts, fp) = HOLogic.strip_ptupleabs split
     val output_names = Name.variant_list (Term.add_free_names body [])
       (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
     val output_frees = rev (map2 (curry Free) output_names Ts)
     val body = subst_bounds (output_frees, body)
     val (pred as Const (name, T), all_args) =