# HG changeset patch
# User haftmann
# Date 1178524687 -7200
# Node ID 3c41e8492ba67b75f30ae09ddb258cf1571b670f
# Parent  f65a76867179c9d32412fbb9dffbb0226225066a
changed 'code nofunc' to 'code func del'

diff -r f65a76867179 -r 3c41e8492ba6 src/HOL/Library/MLString.thy
--- a/src/HOL/Library/MLString.thy	Mon May 07 00:52:25 2007 +0200
+++ b/src/HOL/Library/MLString.thy	Mon May 07 09:58:07 2007 +0200
@@ -26,7 +26,7 @@
 
 datatype ml_string = STR string
 
-lemmas [code nofunc] = ml_string.recs ml_string.cases
+lemmas [code func del] = ml_string.recs ml_string.cases
 
 lemma [code func]: "size (s\<Colon>ml_string) = 0"
   by (cases s) simp_all