src/HOL/Tools/hologic.ML
changeset 39250 548a3e5521ab
parent 38864 4abe644fcea5
child 39756 6c8e83d94536
     1.1 --- a/src/HOL/Tools/hologic.ML	Thu Sep 09 11:10:44 2010 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Thu Sep 09 14:38:14 2010 +0200
     1.3 @@ -596,9 +596,9 @@
     1.4  
     1.5  val literalT = Type ("String.literal", []);
     1.6  
     1.7 -fun mk_literal s = Const ("String.literal.STR", stringT --> literalT)
     1.8 +fun mk_literal s = Const ("String.STR", stringT --> literalT)
     1.9        $ mk_string s;
    1.10 -fun dest_literal (Const ("String.literal.STR", _) $ t) =
    1.11 +fun dest_literal (Const ("String.STR", _) $ t) =
    1.12        dest_string t
    1.13    | dest_literal t = raise TERM ("dest_literal", [t]);
    1.14