src/HOL/Typedef.thy
changeset 29056 dc08e3990c77
parent 28965 1de908189869
child 29608 564ea783ace8
--- a/src/HOL/Typedef.thy	Wed Dec 10 22:05:58 2008 +0100
+++ b/src/HOL/Typedef.thy	Thu Dec 11 00:42:52 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Typedef.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Munich
 *)
 
@@ -116,15 +115,10 @@
 
 end
 
-use "Tools/typedef_package.ML"
-use "Tools/typecopy_package.ML"
-use "Tools/typedef_codegen.ML"
+use "Tools/typedef_package.ML" setup TypedefPackage.setup
+use "Tools/typecopy_package.ML" setup TypecopyPackage.setup
+use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
 
-setup {*
-  TypedefPackage.setup
-  #> TypecopyPackage.setup
-  #> TypedefCodegen.setup
-*}
 
 text {* This class is just a workaround for classes without parameters;
   it shall disappear as soon as possible. *}