src/HOL/BNF_GFP.thy

   then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
   hence "univ f X = f x" using assms univ_commute by fastforce
   thus "univ f X \<in> B" using x PRES by simp
 qed
 
-ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
-ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
 ML_file "Tools/BNF/bnf_gfp_util.ML"
 ML_file "Tools/BNF/bnf_gfp_tactics.ML"
 ML_file "Tools/BNF/bnf_gfp.ML"
+ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
+ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
 
 end