diff -r a0adf838e2d1 -r 6d3fad6f01c9 src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Def.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -157,7 +157,7 @@
 lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
   by clarsimp
 
-ML_file "Tools/bnf_def_tactics.ML"
-ML_file "Tools/bnf_def.ML"
+ML_file "Tools/BNF/bnf_def_tactics.ML"
+ML_file "Tools/BNF/bnf_def.ML"
 
 end