src/HOL/Library/Code_Char.thy

--- a/src/HOL/Library/Code_Char.thy	Thu Sep 09 11:10:44 2010 +0200
+++ b/src/HOL/Library/Code_Char.thy	Thu Sep 09 14:38:14 2010 +0200
@@ -44,14 +44,6 @@
 definition implode :: "string \<Rightarrow> String.literal" where
   "implode = STR"
 
-primrec explode :: "String.literal \<Rightarrow> string" where
-  "explode (STR s) = s"
-
-lemma [code]:
-  "literal_case f s = f (explode s)"
-  "literal_rec f s = f (explode s)"
-  by (cases s, simp)+
-
 code_reserved SML String
 
 code_const implode