# HG changeset patch
# User haftmann
# Date 1256653941 -3600
# Node ID 565ad811db2105f6ddf697c11b4f94ab68b9c9d3
# Parent  ea75c6ea643e54251cb72e1de20117baf7c5d314
tuned

diff -r ea75c6ea643e -r 565ad811db21 src/HOL/String.thy
--- 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")