src/HOL/BNF_GFP.thy
changeset 55538 6a5986170c1d
parent 55463 942c2153b5b4
child 55542 4394bb0b522b
--- a/src/HOL/BNF_GFP.thy	Mon Feb 17 14:59:09 2014 +0100
+++ b/src/HOL/BNF_GFP.thy	Mon Feb 17 18:18:27 2014 +0100
@@ -349,10 +349,10 @@
   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