# HG changeset patch
# User blanchet
# Date 1347376489 -7200
# Node ID 97809ae5f7bb1cc9eb239e063da453ba6b8a7275
# Parent  c057e1b39f162cfdecf7c97f48c12661f7d529fe
move "bnf_util.ML" to "BNF_Util.thy"

diff -r c057e1b39f16 -r 97809ae5f7bb src/HOL/Codatatype/BNF_Def.thy
--- a/src/HOL/Codatatype/BNF_Def.thy	Tue Sep 11 17:09:39 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Def.thy	Tue Sep 11 17:14:49 2012 +0200
@@ -14,8 +14,6 @@
 and
   "bnf_def" :: thy_goal
 uses
-  "Tools/bnf_util.ML"
-  "Tools/bnf_tactics.ML"
   "Tools/bnf_def.ML"
 begin
 
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
diff -r c057e1b39f16 -r 97809ae5f7bb src/HOL/Codatatype/BNF_Wrap.thy
--- a/src/HOL/Codatatype/BNF_Wrap.thy	Tue Sep 11 17:09:39 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Wrap.thy	Tue Sep 11 17:14:49 2012 +0200
@@ -8,7 +8,7 @@
 header {* Wrapping Datatypes *}
 
 theory BNF_Wrap
-imports BNF_Def
+imports BNF_Util
 keywords
   "wrap_data" :: thy_goal
 and
diff -r c057e1b39f16 -r 97809ae5f7bb src/HOL/Codatatype/Codatatype.thy
--- a/src/HOL/Codatatype/Codatatype.thy	Tue Sep 11 17:09:39 2012 +0200
+++ b/src/HOL/Codatatype/Codatatype.thy	Tue Sep 11 17:14:49 2012 +0200
@@ -10,7 +10,7 @@
 header {* The (Co)datatype Package *}
 
 theory Codatatype
-imports BNF_Wrap BNF_LFP BNF_GFP
+imports BNF_LFP BNF_GFP BNF_Wrap
 keywords
   "data" :: thy_decl
 and