# HG changeset patch
# User haftmann
# Date 1184570941 -7200
# Node ID 4e4b92e76219b3260b0d9b47208d10191b4f3816
# Parent  d36e3ffdb5ce59c6d998cd976ad6962257fb3321
fixed SML/NJ int problem

diff -r d36e3ffdb5ce -r 4e4b92e76219 src/HOL/Complex/ex/linreif.ML
--- a/src/HOL/Complex/ex/linreif.ML	Mon Jul 16 09:29:00 2007 +0200
+++ b/src/HOL/Complex/ex/linreif.ML	Mon Jul 16 09:29:01 2007 +0200
@@ -9,7 +9,8 @@
 struct
 
 open Ferrack;
-open ReflectedFerrack
+
+val nat = Ferrack.nat o Integer.int;
 
 exception LINR;
 
@@ -29,7 +30,7 @@
       | Const("RealDef.real",_)$ @{term "1::int"} => C 1
       | @{term "0::real"} => C 0
       | @{term "0::real"} => C 1
-      | Term.Bound i => Bound (Integer.nat i)
+      | Term.Bound i => Bound (nat i)
       | Const(@{const_name "HOL.uminus"},_)$t' => Neg (num_of_term vs t')
       | Const (@{const_name "HOL.plus"},_)$t1$t2 => Add (num_of_term vs t1,num_of_term vs t2)
       | Const (@{const_name "HOL.minus"},_)$t1$t2 => Sub (num_of_term vs t1,num_of_term vs t2)
@@ -69,7 +70,7 @@
 
 fun start_vs t =
     let val fs = term_frees t
-    in zip fs (map Integer.nat (0 upto  (length fs - 1)))
+    in zip fs (map nat (0 upto  (length fs - 1)))
     end ;
 
 (* transform num and fm back to terms *)
diff -r d36e3ffdb5ce -r 4e4b92e76219 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Mon Jul 16 09:29:00 2007 +0200
+++ b/src/HOL/ex/ROOT.ML	Mon Jul 16 09:29:01 2007 +0200
@@ -50,8 +50,7 @@
 time_use_thy "Arith_Examples";
 time_use_thy "Dense_Linear_Order_Ex";
 time_use_thy "PresburgerEx";
-if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
-else time_use_thy "Reflected_Presburger";
+time_use_thy "Reflected_Presburger";
 time_use_thy "BT";
 time_use_thy "InSort";
 time_use_thy "Qsort";
diff -r d36e3ffdb5ce -r 4e4b92e76219 src/HOL/ex/Reflected_Presburger.thy
--- a/src/HOL/ex/Reflected_Presburger.thy	Mon Jul 16 09:29:00 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy	Mon Jul 16 09:29:01 2007 +0200
@@ -1906,8 +1906,9 @@
     (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0)))
       (Bound 2))))))))"
 
+code_reserved SML oo
 code_gen pa cooper_test in SML to GeneratedCooper
-(*code_reserved SML oo code_gen pa in SML to GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*)
+(*code_gen pa in SML to GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*)
 
 ML {* GeneratedCooper.cooper_test () *}
 use "coopereif.ML"
diff -r d36e3ffdb5ce -r 4e4b92e76219 src/HOL/ex/coopereif.ML
--- a/src/HOL/ex/coopereif.ML	Mon Jul 16 09:29:00 2007 +0200
+++ b/src/HOL/ex/coopereif.ML	Mon Jul 16 09:29:01 2007 +0200
@@ -10,6 +10,8 @@
 
 open GeneratedCooper;
 
+val nat = GeneratedCooper.nat o Integer.int;
+
 fun i_of_term vs t = case t
  of Free(xn,xT) => (case AList.lookup (op aconv) vs t
    of NONE   => error "Variable not found in the list!"