src/HOL/Typerep.thy

--- a/src/HOL/Typerep.thy	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/HOL/Typerep.thy	Tue Nov 10 16:04:57 2009 +0100
@@ -50,7 +50,7 @@
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in
     thy
-    |> TheoryTarget.instantiation ([tyco], vs, @{sort typerep})
+    |> Theory_Target.instantiation ([tyco], vs, @{sort typerep})
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
     |> snd