src/HOL/Typerep.thy

--- a/src/HOL/Typerep.thy	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Typerep.thy	Wed Aug 11 14:31:43 2010 +0200
@@ -56,7 +56,7 @@
     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