--- a/src/HOL/HOLCF/Domain_Aux.thy Sun Jan 06 13:44:33 2019 +0100
+++ b/src/HOL/HOLCF/Domain_Aux.thy Sun Jan 06 15:04:34 2019 +0100
@@ -355,10 +355,10 @@
named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)"
and domain_map_ID "theorems like foo_map$ID = ID"
-ML_file "Tools/Domain/domain_take_proofs.ML"
-ML_file "Tools/cont_consts.ML"
-ML_file "Tools/cont_proc.ML"
-ML_file "Tools/Domain/domain_constructors.ML"
-ML_file "Tools/Domain/domain_induction.ML"
+ML_file \<open>Tools/Domain/domain_take_proofs.ML\<close>
+ML_file \<open>Tools/cont_consts.ML\<close>
+ML_file \<open>Tools/cont_proc.ML\<close>
+ML_file \<open>Tools/Domain/domain_constructors.ML\<close>
+ML_file \<open>Tools/Domain/domain_induction.ML\<close>
end