src/HOL/Tools/Ctr_Sugar/case_translation.ML

     val constrs = Variable.polymorphic ctxt raw_constrs;
     val case_key = case_comb |> dest_Const |> fst;
     val constr_keys = map (fst o dest_Const) constrs;
     val data = (case_comb, constrs);
     val Tname = Tname_of_data data;
-    val update_constrs =
-      fold (fn key => Symtab.insert_list (eq_fst (op =)) (key, (Tname, data))) constr_keys;
-    val update_cases = Symtab.default (case_key, data);
+    val update_constrs = fold (fn key => Symtab.cons_list (key, (Tname, data))) constr_keys;
+    val update_cases = Symtab.update (case_key, data);
   in
     context
     |> map_constrs update_constrs
     |> map_cases update_cases
   end;