# HG changeset patch
# User chaieb
# Date 1126809527 -7200
# Node ID acfc05e02e5bf87114c9a7b55d743cbd577a3154
# Parent  67c84a7d29f79eabaf40b3ff9c4672222da79b69
getting it work for SMLNJ

diff -r 67c84a7d29f7 -r acfc05e02e5b src/HOL/Integ/reflected_presburger.ML
--- a/src/HOL/Integ/reflected_presburger.ML	Thu Sep 15 20:27:48 2005 +0200
+++ b/src/HOL/Integ/reflected_presburger.ML	Thu Sep 15 20:38:47 2005 +0200
@@ -52,7 +52,7 @@
     (if (c = 0) then Cst 0
       else Add (Mult (Cst (c * c'), Var n), lin_mul (c, r)));
 
-fun op_60_def0 m n = ((m) < (n));
+fun op_60_def0 m n = IntInf.< (m,n);
 
 fun op_60_61_def0 m n = not (op_60_def0 n m);
 
@@ -174,7 +174,7 @@
   | nnf (NOT (Equ (p, q))) =
     Or (And (nnf p, nnf (NOT q)), And (nnf (NOT p), nnf q));
 
-fun op_45_def2 z w = (z + ~ w);
+fun op_45_def2 z w =  IntInf.+ (z,~ w);
 
 fun op_45_def0 m n = nat (op_45_def2 (m) (n));
 
@@ -215,7 +215,7 @@
 
 fun split x = (fn p => x (fst p) (snd p));
 
-fun negateSnd x = split (fn q => fn r => (q, ~ r)) x;
+fun negateSnd x = split (fn q => fn r => (q, IntInf.~ r)) x;
 
 fun adjust b =
   (fn (q:IntInf.int, r:IntInf.int) =>
@@ -240,7 +240,7 @@
                    else negateSnd (posDivAlg (~ a, ~ b)))))
     x;
 
-fun op_mod_def1 (a:IntInf.int) (b:IntInf.int) = snd (divAlg (a, b));
+fun op_mod_def1 a b = snd (divAlg (a, b));
 
 fun op_dvd m n = (op_mod_def1 n m = 0);
 
@@ -1139,9 +1139,9 @@
   | minusinf (QAll ap) = QAll ap
   | minusinf (QEx aq) = QEx aq;
 
-fun (abs: IntInf.int -> IntInf.int) i = (if (i < 0) then ~ i else i);
+fun abs (i:IntInf.int) = (if (i < 0) then IntInf.~ i else i);
 
-fun op_div_def1 (a:IntInf.int) (b:IntInf.int) = fst (divAlg (a, b));
+fun op_div_def1 a b = fst (divAlg (a, b));
 
 fun op_mod_def0 m n = nat (op_mod_def1 (m) (n));
 
diff -r 67c84a7d29f7 -r acfc05e02e5b src/HOL/Tools/Presburger/reflected_presburger.ML
--- a/src/HOL/Tools/Presburger/reflected_presburger.ML	Thu Sep 15 20:27:48 2005 +0200
+++ b/src/HOL/Tools/Presburger/reflected_presburger.ML	Thu Sep 15 20:38:47 2005 +0200
@@ -52,7 +52,7 @@
     (if (c = 0) then Cst 0
       else Add (Mult (Cst (c * c'), Var n), lin_mul (c, r)));
 
-fun op_60_def0 m n = ((m) < (n));
+fun op_60_def0 m n = IntInf.< (m,n);
 
 fun op_60_61_def0 m n = not (op_60_def0 n m);
 
@@ -174,7 +174,7 @@
   | nnf (NOT (Equ (p, q))) =
     Or (And (nnf p, nnf (NOT q)), And (nnf (NOT p), nnf q));
 
-fun op_45_def2 z w = (z + ~ w);
+fun op_45_def2 z w =  IntInf.+ (z,~ w);
 
 fun op_45_def0 m n = nat (op_45_def2 (m) (n));
 
@@ -215,7 +215,7 @@
 
 fun split x = (fn p => x (fst p) (snd p));
 
-fun negateSnd x = split (fn q => fn r => (q, ~ r)) x;
+fun negateSnd x = split (fn q => fn r => (q, IntInf.~ r)) x;
 
 fun adjust b =
   (fn (q:IntInf.int, r:IntInf.int) =>
@@ -240,7 +240,7 @@
                    else negateSnd (posDivAlg (~ a, ~ b)))))
     x;
 
-fun op_mod_def1 (a:IntInf.int) (b:IntInf.int) = snd (divAlg (a, b));
+fun op_mod_def1 a b = snd (divAlg (a, b));
 
 fun op_dvd m n = (op_mod_def1 n m = 0);
 
@@ -1139,9 +1139,9 @@
   | minusinf (QAll ap) = QAll ap
   | minusinf (QEx aq) = QEx aq;
 
-fun (abs: IntInf.int -> IntInf.int) i = (if (i < 0) then ~ i else i);
+fun abs (i:IntInf.int) = (if (i < 0) then IntInf.~ i else i);
 
-fun op_div_def1 (a:IntInf.int) (b:IntInf.int) = fst (divAlg (a, b));
+fun op_div_def1 a b = fst (divAlg (a, b));
 
 fun op_mod_def0 m n = nat (op_mod_def1 (m) (n));