# HG changeset patch
# User wenzelm
# Date 1186083907 -7200
# Node ID 75063f96618f50072bf3736e2a480060adb06a5a
# Parent  dc95373bd69f15efb933a68f42b682421282d40b
added int type constraints to accomodate hacked SML/NJ;

diff -r dc95373bd69f -r 75063f96618f src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Aug 02 21:43:55 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Aug 02 21:45:07 2007 +0200
@@ -204,7 +204,7 @@
 fun coind_prefix true = "co"
   | coind_prefix false = "";
 
-fun log b m n = if m >= n then 0 else 1 + log b (b * m) n;
+fun log (b:int) m n = if m >= n then 0 else 1 + log b (b * m) n;
 
 fun make_bool_args f g [] i = []
   | make_bool_args f g (x :: xs) i =
diff -r dc95373bd69f -r 75063f96618f src/Pure/ProofGeneral/pgip_types.ML
--- a/src/Pure/ProofGeneral/pgip_types.ML	Thu Aug 02 21:43:55 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Thu Aug 02 21:45:07 2007 +0200
@@ -188,7 +188,7 @@
        | _ => raise PGIP ("Invalid boolean value: " ^ quote s))
 
 local
-    fun int_in_range (NONE,NONE) _ = true
+    fun int_in_range (NONE,NONE) (_: int) = true
       | int_in_range (SOME min,NONE) i = min<= i
       | int_in_range (NONE,SOME max) i = i<=max
       | int_in_range (SOME min,SOME max) i = min<= i andalso i<=max
diff -r dc95373bd69f -r 75063f96618f src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Aug 02 21:43:55 2007 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Aug 02 21:45:07 2007 +0200
@@ -412,7 +412,7 @@
   Graph.topological_order tasks
   |> List.app (fn name => (case Graph.get_node tasks name of Task.Task f => f () | _ => ()));
 
-fun max_task (task as (_, (Task.Task _, _))) NONE = SOME task
+fun max_task (task as (_, (Task.Task _, _: int))) NONE = SOME task
   | max_task (task as (_, (Task.Task _, m))) (task' as SOME (_, (_, m'))) =
       if m > m' then SOME task else task'
   | max_task _ task' = task';
diff -r dc95373bd69f -r 75063f96618f src/Tools/Metis/metis.ML
--- a/src/Tools/Metis/metis.ML	Thu Aug 02 21:43:55 2007 +0200
+++ b/src/Tools/Metis/metis.ML	Thu Aug 02 21:45:07 2007 +0200
@@ -5386,7 +5386,7 @@
     | range NONE (SOME j) = "{n IN Z | n <= " ^ Int.toString j ^ "}"
     | range (SOME i) (SOME j) =
     "{n IN Z | " ^ Int.toString i ^ " <= n <= " ^ Int.toString j ^ "}";
-  fun oLeq (SOME x) (SOME y) = x <= y | oLeq _ _ = true;
+  fun oLeq (SOME (x:int)) (SOME y) = x <= y | oLeq _ _ = true;
   fun argToInt arg omin omax x =
     (case Int.fromString x of
        SOME i =>