src/ZF/Bin.thy

--- a/src/ZF/Bin.thy	Sun Jan 06 13:44:33 2019 +0100
+++ b/src/ZF/Bin.thy	Sun Jan 06 15:04:34 2019 +0100
@@ -117,7 +117,7 @@
   "_Int" :: "num_token => i"  (\<open>#_\<close> 1000)
   "_Neg_Int" :: "num_token => i"  (\<open>#-_\<close> 1000)
 
-ML_file "Tools/numeral_syntax.ML"
+ML_file \<open>Tools/numeral_syntax.ML\<close>
 
 
 declare bin.intros [simp,TC]
@@ -698,7 +698,7 @@
   apply (simp add: zadd_ac)
   done
 
-ML_file "int_arith.ML"
+ML_file \<open>int_arith.ML\<close>
 
 subsection \<open>examples:\<close>