--- 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 =
--- 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
--- 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';
--- 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 =>