# HG changeset patch
# User berghofe
# Date 1014632827 -3600
# Node ID b85c62c4e82679b5b5e61997f429c8f1b8aac9e3
# Parent  3bda5306d26247c4c3e12dab173e83fde551e7b0
Introduced variants of operators + * ~ constrained to type int
(to make SML/NJ happy).

diff -r 3bda5306d262 -r b85c62c4e826 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Mon Feb 25 10:45:22 2002 +0100
+++ b/src/HOL/Integ/NatBin.thy	Mon Feb 25 11:27:07 2002 +0100
@@ -62,6 +62,15 @@
 
 subsection {* Configuration of the code generator *}
 
+ML {*
+infix 7 `*;
+infix 6 `+;
+
+val op `* = op * : int * int -> int;
+val op `+ = op + : int * int -> int;
+val `~ = ~ : int -> int;
+*}
+
 types_code
   "int" ("int")
 
@@ -73,9 +82,9 @@
 consts_code
   "0" :: "int"                  ("0")
   "1" :: "int"                  ("1")
-  "uminus" :: "int => int"      ("~")
-  "op +" :: "int => int => int" ("(_ +/ _)")
-  "op *" :: "int => int => int" ("(_ */ _)")
+  "uminus" :: "int => int"      ("`~")
+  "op +" :: "int => int => int" ("(_ `+/ _)")
+  "op *" :: "int => int => int" ("(_ `*/ _)")
   "neg"                         ("(_ < 0)")
 
 end