diff -r f6b0d827240e -r bdc1e2f0a86a src/HOL/ex/Eval_Examples.thy
--- a/src/HOL/ex/Eval_Examples.thy	Tue Sep 01 17:25:36 2015 +0200
+++ b/src/HOL/ex/Eval_Examples.thy	Tue Sep 01 22:32:58 2015 +0200
@@ -43,7 +43,7 @@
 text {* a fancy datatype *}
 
 datatype ('a, 'b) foo =
-    Foo "'a\<Colon>order" 'b
+    Foo "'a::order" 'b
   | Bla "('a, 'b) bar"
   | Dummy nat
 and ('a, 'b) bar =