diff -r cf7f3465eaf1 -r 240563fbf41d src/Sequents/Washing.thy
--- a/src/Sequents/Washing.thy	Thu Jul 23 14:20:51 2015 +0200
+++ b/src/Sequents/Washing.thy	Thu Jul 23 14:25:05 2015 +0200
@@ -32,10 +32,10 @@
 
 (* "activate" definitions for use in proof *)
 
-ML {* ML_Thms.bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}]))) *}
-ML {* ML_Thms.bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}]))) *}
-ML {* ML_Thms.bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}]))) *}
-ML {* ML_Thms.bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}]))) *}
+ML \<open>ML_Thms.bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}])))\<close>
+ML \<open>ML_Thms.bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}])))\<close>
+ML \<open>ML_Thms.bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}])))\<close>
+ML \<open>ML_Thms.bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}])))\<close>
 
 (* a load of dirty clothes and two dollars gives you clean clothes *)