diff -r 922e702ae8ca -r 702085ca8564 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Thu Mar 03 23:33:41 2016 +0100
+++ b/src/HOL/Tools/hologic.ML	Fri Feb 26 22:38:44 2016 +0100
@@ -644,9 +644,9 @@
 
 val literalT = Type ("String.literal", []);
 
-fun mk_literal s = Const ("String.STR", stringT --> literalT)
+fun mk_literal s = Const ("String.literal.STR", stringT --> literalT)
       $ mk_string s;
-fun dest_literal (Const ("String.STR", _) $ t) =
+fun dest_literal (Const ("String.literal.STR", _) $ t) =
       dest_string t
   | dest_literal t = raise TERM ("dest_literal", [t]);