src/Tools/Code_Generator.thy

 ML_file "~~/src/Tools/Code/code_namespace.ML"
 ML_file "~~/src/Tools/Code/code_ml.ML"
 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))"
 
 lemma holds: "PROP holds"

 ML_file "~~/src/Tools/nbe.ML"
 
 hide_const (open) holds
 
 end
-