diff -r acc2f1801acc -r 57752a91eec4 src/HOL/ex/Reflection_Examples.thy
--- a/src/HOL/ex/Reflection_Examples.thy	Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/ex/Reflection_Examples.thy	Thu Sep 11 18:54:36 2014 +0200
@@ -17,7 +17,7 @@
 often need its structure.  Traditionnaly such simplifications are written in ML,
 proofs are synthesized.
 
-An other strategy is to declare an HOL-datatype @{text \<tau>} and an HOL function (the
+An other strategy is to declare an HOL datatype @{text \<tau>} and an HOL function (the
 interpretation) that maps elements of @{text \<tau>} to elements of @{text \<sigma>}.
 
 The functionality of @{text reify} then is, given a term @{text t} of type @{text \<sigma>},