# HG changeset patch
# User haftmann
# Date 1190790358 -7200
# Node ID 16b11ba363507166ad5525381c6b31d5ecb82ca8
# Parent  56ba87ec8d31acea976bd6f9a9e0f23bda0ec125
made SML/NJ happy

diff -r 56ba87ec8d31 -r 16b11ba36350 src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Tue Sep 25 21:08:36 2007 +0200
+++ b/src/HOL/ex/Codegenerator.thy	Wed Sep 26 09:05:58 2007 +0200
@@ -11,6 +11,7 @@
 ML {* (*FIXME get rid of this*)
 nonfix union;
 nonfix inter;
+nonfix upto;
 *}
 
 export_code * in SML module_name CodegenTest
@@ -20,6 +21,7 @@
 ML {*
 infix union;
 infix inter;
+infix 4 upto;
 *}
 
 end