diff -r d80b2df54d31 -r a96320074298 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Sun Jan 06 13:44:33 2019 +0100
+++ b/src/HOL/Lifting.thy	Sun Jan 06 15:04:34 2019 +0100
@@ -552,22 +552,22 @@
 
 subsection \<open>ML setup\<close>
 
-ML_file "Tools/Lifting/lifting_util.ML"
+ML_file \<open>Tools/Lifting/lifting_util.ML\<close>
 
 named_theorems relator_eq_onp
   "theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate"
-ML_file "Tools/Lifting/lifting_info.ML"
+ML_file \<open>Tools/Lifting/lifting_info.ML\<close>
 
 (* setup for the function type *)
 declare fun_quotient[quot_map]
 declare fun_mono[relator_mono]
 lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2
 
-ML_file "Tools/Lifting/lifting_bnf.ML"
-ML_file "Tools/Lifting/lifting_term.ML"
-ML_file "Tools/Lifting/lifting_def.ML"
-ML_file "Tools/Lifting/lifting_setup.ML"
-ML_file "Tools/Lifting/lifting_def_code_dt.ML"
+ML_file \<open>Tools/Lifting/lifting_bnf.ML\<close>
+ML_file \<open>Tools/Lifting/lifting_term.ML\<close>
+ML_file \<open>Tools/Lifting/lifting_def.ML\<close>
+ML_file \<open>Tools/Lifting/lifting_setup.ML\<close>
+ML_file \<open>Tools/Lifting/lifting_def_code_dt.ML\<close>
 
 lemma pred_prod_beta: "pred_prod P Q xy \<longleftrightarrow> P (fst xy) \<and> Q (snd xy)"
 by(cases xy) simp