# HG changeset patch
# User haftmann
# Date 1188196261 -7200
# Node ID d555d941f983cc3f819036177822d29c0d903bb5
# Parent  02d29baa42ff7acb475e2f7380a54c000e50ed8f
circumvented infix problem

diff -r 02d29baa42ff -r d555d941f983 src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Sun Aug 26 21:28:08 2007 +0200
+++ b/src/HOL/ex/Codegenerator.thy	Mon Aug 27 08:31:01 2007 +0200
@@ -8,7 +8,7 @@
 imports ExecutableContent
 begin
 
-ML {*
+ML {* (*FIXME get rid of this*)
 nonfix union;
 nonfix inter;
 *}
@@ -17,4 +17,9 @@
   in OCaml file -
   in Haskell file -
 
+ML {*
+infix union;
+infix inter;
+*}
+
 end