src/HOL/Typerep.thy

     val rhs = @{term Typerep} $ HOLogic.mk_literal tyco
       $ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs);
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in
     thy
-    |> Theory_Target.instantiation ([tyco], vs, @{sort typerep})
+    |> Class.instantiation ([tyco], vs, @{sort typerep})
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
     |> snd
     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   end;