fixed code_generate syntax;
authorwenzelm
Tue, 24 Jan 2006 00:44:39 +0100
changeset 18772 f0dd51087eb3
parent 18771 63efe00371af
child 18773 0eabf66582d0
fixed code_generate syntax;
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")