src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

     val U = fastype_of success_t;
     val U' = dest_monadT compfuns U;
     val v = Free (name, T);
     val v' = Free (name', T);
   in
-    lambda v (Datatype_Case.make_case ctxt Datatype_Case.Quiet [] v
+    lambda v (Datatype_Case.make_case ctxt Datatype_Case.Quiet Name.context v
       [(HOLogic.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_empty compfuns U'),

             val compilation = the_default (mk_empty compfuns (HOLogic.mk_tupleT outTs))
               (compile_switch_tree (argnames @ x :: all_vs) ctxt_eqs' switched)
         in
           (pattern, compilation)
         end
-        val switch = Datatype_Case.make_case ctxt Datatype_Case.Quiet [] inp_var
+        val switch = Datatype_Case.make_case ctxt Datatype_Case.Quiet Name.context inp_var
           ((map compile_single_case switched_clauses) @
             [(xt, mk_empty compfuns (HOLogic.mk_tupleT outTs))])
       in
         case compile_switch_tree all_vs ctxt_eqs left_clauses of
           NONE => SOME switch