--- 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]);