# HG changeset patch
# User haftmann
# Date 1175430528 -7200
# Node ID c233923bbabe1614dc89b89ff73d95b04043bb8f
# Parent  6775c71f1da0226114d2638efda5a5934618c8ab
added reserved words mod, div for SML

diff -r 6775c71f1da0 -r c233923bbabe src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Sat Mar 31 15:13:52 2007 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Sun Apr 01 14:28:48 2007 +0200
@@ -2004,7 +2004,8 @@
         pr_typ (INFX (1, R)) ty2
       ]))
   (*IntInt resp. Big_int are added later when code extraction for numerals is set up*)
-  #> add_reserved "SML" "o" (*dictionary projections use it already*)
+  #> fold (add_reserved "SML") ["o" (*dictionary projections use it already*),
+      "div", "mod" (*infixes*)]
   #> fold (add_reserved "Haskell") [
       "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
       "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",