src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

     val U' = dest_predT compfuns U;
     val v = Free (name, T);
     val v' = Free (name', T);
   in
     lambda v (fst (Datatype.make_case
-      (ProofContext.init thy) false [] v
+      (ProofContext.init thy) DatatypeCase.Quiet [] v
       [(mk_tuple out_ts,
         if null eqs'' then success_t
         else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
           foldr1 HOLogic.mk_conj eqs'' $ success_t $
             mk_bot compfuns U'),