diff -r 03f8dcab55f3 -r 25bd3ed2ac9f src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Jan 04 14:09:56 2010 +0100
+++ b/src/Pure/sign.ML	Mon Jan 04 14:09:56 2010 +0100
@@ -151,7 +151,6 @@
 structure SignData = TheoryDataFun
 (
   type T = sign;
-  val copy = I;
   fun extend (Sign {syn, tsig, consts, ...}) =
     make_sign (Name_Space.default_naming, syn, tsig, consts);