src/HOL/Codatatype/BNF_Wrap.thy
changeset 49309 f20b24214ac2
parent 49286 dde4967c9233
child 49312 c874ff5658dc
--- a/src/HOL/Codatatype/BNF_Wrap.thy	Wed Sep 12 05:03:18 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Wrap.thy	Wed Sep 12 05:21:47 2012 +0200
@@ -12,9 +12,9 @@
 keywords
   "wrap_data" :: thy_goal and
   "no_dests"
-uses
-  "Tools/bnf_wrap_tactics.ML"
-  "Tools/bnf_wrap.ML"
 begin
 
+ML_file "Tools/bnf_wrap_tactics.ML"
+ML_file "Tools/bnf_wrap.ML"
+
 end