diff -r 438703674711 -r 321e220a6baa ProgTutorial/Readme.thy
--- a/ProgTutorial/Readme.thy	Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Readme.thy	Tue May 21 16:22:30 2019 +0200
@@ -160,7 +160,7 @@
 
 So as a rule of thumb, to facilitate result checking use prefer this order:
 \begin{enumerate}
- \item \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close>
+ \item \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close>    
  \item \<open>@{ML_response \<open>expr\<close> \<open>string\<close>}\<close>
  \item \<open>@{ML_matchresult_fake \<open>expr\<close> \<open>pat\<close>}\<close> or \<open>@{ML_response \<open>expr\<close>}\<close>
  \item \<open>@{ML_matchresult_fake_both \<open>expr\<close> \<open>pat\<close>}\<close>