# HG changeset patch
# User wenzelm
# Date 1138059879 -3600
# Node ID f0dd51087eb3315c7524f327fb4e946c4c5c1b44
# Parent  63efe00371afe45f0de32f6c79961de7e3ec0feb
fixed code_generate syntax;

diff -r 63efe00371af -r f0dd51087eb3 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Tue Jan 24 00:43:34 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Tue Jan 24 00:44:39 2006 +0100
@@ -62,7 +62,7 @@
 fun Ball S P = Library.forall P S;
 *}
 
-code_generate "op mem"
+code_generate ("op mem")
 
 code_primconst "insert"
   depending_on ("List.const.member")