diff -r f6b0d827240e -r bdc1e2f0a86a src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Tue Sep 01 17:25:36 2015 +0200
+++ b/src/Tools/Code_Generator.thy	Tue Sep 01 22:32:58 2015 +0200
@@ -26,7 +26,7 @@
 ML_file "~~/src/Tools/Code/code_haskell.ML"
 ML_file "~~/src/Tools/Code/code_scala.ML"
 
-code_datatype "TYPE('a\<Colon>{})"
+code_datatype "TYPE('a::{})"
 
 definition holds :: "prop" where
   "holds \<equiv> ((\<lambda>x::prop. x) \<equiv> (\<lambda>x. x))"
@@ -59,4 +59,3 @@
 hide_const (open) holds
 
 end
-