--- a/src/HOL/Typedef.thy Tue Aug 29 14:31:12 2006 +0200
+++ b/src/HOL/Typedef.thy Tue Aug 29 14:31:13 2006 +0200
@@ -7,7 +7,10 @@
theory Typedef
imports Set
-uses ("Tools/typedef_package.ML") ("Tools/typedef_codegen.ML")
+uses
+ ("Tools/typedef_package.ML")
+ ("Tools/typecopy_package.ML")
+ ("Tools/typedef_codegen.ML")
begin
locale type_definition =
@@ -83,8 +86,13 @@
qed
use "Tools/typedef_package.ML"
+use "Tools/typecopy_package.ML"
use "Tools/typedef_codegen.ML"
-setup {* TypedefPackage.setup #> TypedefCodegen.setup *}
+setup {*
+ TypedefPackage.setup
+ #> TypecopyPackage.setup
+ #> TypedefCodegen.setup
+*}
end