--- a/src/HOL/BNF_Greatest_Fixpoint.thy Sun Jan 06 13:44:33 2019 +0100
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy Sun Jan 06 15:04:34 2019 +0100
@@ -281,10 +281,10 @@
thus "univ f X \<in> B" using x PRES by simp
qed
-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"
+ML_file \<open>Tools/BNF/bnf_gfp_util.ML\<close>
+ML_file \<open>Tools/BNF/bnf_gfp_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_gfp.ML\<close>
+ML_file \<open>Tools/BNF/bnf_gfp_rec_sugar_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_gfp_rec_sugar.ML\<close>
end