src/HOL/Codatatype/BNF_Def.thy

--- a/src/HOL/Codatatype/BNF_Def.thy	Wed Sep 12 05:03:18 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Def.thy	Wed Sep 12 05:21:47 2012 +0200
@@ -12,9 +12,9 @@
 keywords
   "print_bnfs" :: diag and
   "bnf_def" :: thy_goal
-uses
-  "Tools/bnf_def_tactics.ML"
-  "Tools/bnf_def.ML"
 begin
 
+ML_file "Tools/bnf_def_tactics.ML"
+ML_file"Tools/bnf_def.ML"
+
 end