1.1 --- a/src/HOL/Library/Code_Char.thy	Thu Sep 09 11:10:44 2010 +0200
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Thu Sep 09 14:38:14 2010 +0200
     1.3 @@ -44,14 +44,6 @@
     1.4  definition implode :: "string \<Rightarrow> String.literal" where
     1.5    "implode = STR"
     1.6  
     1.7 -primrec explode :: "String.literal \<Rightarrow> string" where
     1.8 -  "explode (STR s) = s"
     1.9 -
    1.10 -lemma [code]:
    1.11 -  "literal_case f s = f (explode s)"
    1.12 -  "literal_rec f s = f (explode s)"
    1.13 -  by (cases s, simp)+
    1.14 -
    1.15  code_reserved SML String
    1.16  
    1.17  code_const implode