| changeset 38536 | 7e57a0dcbd4f |
| parent 38393 | 7c045c03598f |
| child 41732 | 996b0c14a430 |
--- a/src/HOL/Typedef.thy Tue Aug 17 16:44:21 2010 +0200 +++ b/src/HOL/Typedef.thy Tue Aug 17 16:44:24 2010 +0200 @@ -6,9 +6,7 @@ theory Typedef imports Set -uses - ("Tools/typedef.ML") - ("Tools/typedef_codegen.ML") +uses ("Tools/typedef.ML") begin ML {* @@ -115,6 +113,5 @@ end use "Tools/typedef.ML" setup Typedef.setup -use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup end