diff -r c057e1b39f16 -r 97809ae5f7bb src/HOL/Codatatype/BNF_Util.thy
--- a/src/HOL/Codatatype/BNF_Util.thy	Tue Sep 11 17:09:39 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Util.thy	Tue Sep 11 17:14:49 2012 +0200
@@ -13,6 +13,8 @@
   "../Ordinals_and_Cardinals/Cardinal_Arithmetic"
   "~~/src/HOL/Library/Prefix_Order"
   Equiv_Relations_More
+uses
+  ("Tools/bnf_util.ML")
 begin
 
 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
@@ -851,4 +853,7 @@
 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
 by simp
 
+ML_file "Tools/bnf_util.ML"
+ML_file "Tools/bnf_tactics.ML"
+
 end