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