--- a/src/HOL/String.thy Tue Oct 27 15:32:21 2009 +0100
+++ b/src/HOL/String.thy Tue Oct 27 15:32:21 2009 +0100
@@ -155,7 +155,7 @@
datatype literal = STR string
-lemmas [code del] = literal.recs literal.cases
+declare literal.cases [code del] literal.recs [code del]
lemma [code]: "size (s\<Colon>literal) = 0"
by (cases s) simp_all
@@ -168,6 +168,9 @@
use "Tools/string_code.ML"
+code_reserved SML string
+code_reserved OCaml string
+
code_type literal
(SML "string")
(OCaml "string")
@@ -185,9 +188,6 @@
(OCaml "!((_ : string) = _)")
(Haskell infixl 4 "==")
-code_reserved SML string
-code_reserved OCaml string
-
types_code
"char" ("string")