src/HOL/String.thy
changeset 36176 3fe7e97ccca8
parent 35123 e286d5df187a
child 37743 0a3fa8fbcdc5
--- a/src/HOL/String.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/String.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -217,6 +217,6 @@
 in Codegen.add_codegen "char_codegen" char_codegen end
 *}
 
-hide (open) type literal
+hide_type (open) literal
 
 end
\ No newline at end of file