circumvented infix problem
authorhaftmann
Mon, 27 Aug 2007 08:31:01 +0200
changeset 24432 d555d941f983
parent 24431 02d29baa42ff
child 24433 4a405457e9d6
circumvented infix problem
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