src/HOL/String.thy

--- a/src/HOL/String.thy	Mon Jun 10 20:43:17 2013 +0200
+++ b/src/HOL/String.thy	Tue Jun 11 21:07:53 2013 +0200
@@ -382,6 +382,11 @@
 
 end
 
+lemma [code nbe]:
+  fixes s :: "String.literal"
+  shows "HOL.equal s s \<longleftrightarrow> True"
+  by (simp add: equal)
+
 lemma STR_inject' [simp]:
   "STR xs = STR ys \<longleftrightarrow> xs = ys"
   by (simp add: STR_inject)