src/HOL/Tools/string_code.ML
changeset 31205 98370b26c2ce
parent 31055 2cf6efca6c71
child 33989 cb136b5f6050
     1.1 --- a/src/HOL/Tools/string_code.ML	Tue May 19 13:57:51 2009 +0200
     1.2 +++ b/src/HOL/Tools/string_code.ML	Tue May 19 16:54:55 2009 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  sig
     1.5    val add_literal_list_string: string -> theory -> theory
     1.6    val add_literal_char: string -> theory -> theory
     1.7 -  val add_literal_message: string -> theory -> theory
     1.8 +  val add_literal_string: string -> theory -> theory
     1.9  end;
    1.10  
    1.11  structure String_Code : STRING_CODE =
    1.12 @@ -72,7 +72,7 @@
    1.13      @{const_name Char} (SOME (2, (cs_nibbles, pretty)))
    1.14    end;
    1.15  
    1.16 -fun add_literal_message target =
    1.17 +fun add_literal_string target =
    1.18    let
    1.19      fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
    1.20        case List_Code.implode_list nil' cons' t