--- a/src/HOL/Tools/record_package.ML	Wed May 13 18:41:38 2009 +0200
+++ b/src/HOL/Tools/record_package.ML	Wed May 13 18:41:39 2009 +0200
@@ -1464,7 +1464,7 @@
     val tname = Binding.name (Long_Name.base_name name);
   in
     thy
-    |> TypecopyPackage.add_typecopy (Binding.suffix_name ext_typeN tname, alphas) repT NONE
+    |> TypecopyPackage.typecopy (Binding.suffix_name ext_typeN tname, alphas) repT NONE
     |-> (fn (name, _) => `(fn thy => get_thms thy name))
   end;