src/HOL/Tools/Datatype/datatype_codegen.ML

           [((prefix dtco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
             ((prefix dtco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])])
       #> snd
   in
     thy
-    |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
+    |> Class.instantiation (dtcos, vs, [HOLogic.class_eq])
     |> fold_map add_def dtcos
     |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
          (fn _ => fn def_thms => tac def_thms) def_thms)
     |-> (fn def_thms => fold Code.del_eqn def_thms)
     |> fold add_eq_thms dtcos