src/HOL/Codatatype/BNF_LFP.thy
changeset 49309 f20b24214ac2
parent 49308 6190b701e4f4
child 49312 c874ff5658dc
--- a/src/HOL/Codatatype/BNF_LFP.thy	Wed Sep 12 05:03:18 2012 +0200
+++ b/src/HOL/Codatatype/BNF_LFP.thy	Wed Sep 12 05:21:47 2012 +0200
@@ -12,10 +12,10 @@
 keywords
   "data_raw" :: thy_decl and
   "data" :: thy_decl
-uses
-  "Tools/bnf_lfp_util.ML"
-  "Tools/bnf_lfp_tactics.ML"
-  "Tools/bnf_lfp.ML"
 begin
 
+ML_file "Tools/bnf_lfp_util.ML"
+ML_file "Tools/bnf_lfp_tactics.ML"
+ML_file "Tools/bnf_lfp.ML"
+
 end