src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML

 fun mk_case_distinct_ctrs_tac ctxt distincts =
   REPEAT_DETERM o etac ctxt exE THEN' etac ctxt conjE THEN' full_simp_tac (ss_only distincts ctxt);
 
 fun mk_case_tac ctxt n k case_def injects distinctss =
   let
-    val case_def' = mk_unabs_def (n + 1) (case_def RS meta_eq_to_obj_eq);
+    val case_def' = mk_unabs_def (n + 1) (HOLogic.mk_obj_eq case_def);
     val ks = 1 upto n;
   in
     HEADGOAL (rtac ctxt (case_def' RS trans) THEN' rtac ctxt @{thm the_equality} THEN'
       rtac ctxt (mk_disjIN n k) THEN' REPEAT_DETERM o rtac ctxt exI THEN' rtac ctxt conjI THEN'
       rtac ctxt refl THEN' rtac ctxt refl THEN'