--- a/src/HOL/Tools/datatype_realizer.ML Thu Jul 05 00:06:13 2007 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Thu Jul 05 00:06:14 2007 +0200
@@ -97,7 +97,7 @@
fun mk_proj j [] t = t
| mk_proj j (i :: is) t = if null is then t else
- if j = i then HOLogic.mk_fst t
+ if (j: int) = i then HOLogic.mk_fst t
else mk_proj j is (HOLogic.mk_snd t);
val tnames = DatatypeProp.make_tnames recTs;
--- a/src/HOL/Tools/inductive_package.ML Thu Jul 05 00:06:13 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML Thu Jul 05 00:06:14 2007 +0200
@@ -194,7 +194,7 @@
| find_arg T x ((p as (_, (SOME _, _))) :: ps) =
apsnd (cons p) (find_arg T x ps)
| find_arg T x ((p as (U, (NONE, y))) :: ps) =
- if T = U then (y, (U, (SOME x, y)) :: ps)
+ if (T: typ) = U then (y, (U, (SOME x, y)) :: ps)
else apsnd (cons p) (find_arg T x ps);
fun make_args Ts xs =
--- a/src/HOL/Tools/inductive_realizer.ML Thu Jul 05 00:06:13 2007 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Jul 05 00:06:14 2007 +0200
@@ -236,7 +236,7 @@
end;
fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
- if name = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
+ if (name: string) = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
else x;
fun add_dummies f [] _ thy =
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Jul 05 00:06:13 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Thu Jul 05 00:06:14 2007 +0200
@@ -499,7 +499,7 @@
end;
fun coeff poly atom =
- AList.lookup (op =) poly atom |> the_default (0: integer);
+ AList.lookup (op aconv) poly atom |> the_default (0: integer);
fun lcms ks = fold Integer.lcm ks 1;
--- a/src/Provers/order.ML Thu Jul 05 00:06:13 2007 +0200
+++ b/src/Provers/order.ML Thu Jul 05 00:06:14 2007 +0200
@@ -644,7 +644,7 @@
val yi = getIndex y ntc
fun lookup k [] = raise Cannot
- | lookup k ((h,l)::us) = if k = h then l else lookup k us;
+ | lookup k ((h: int,l)::us) = if k = h then l else lookup k us;
fun rev_completeComponentPath y' =
let val edge = lookup (getIndex y' ntc) predlist
@@ -974,7 +974,7 @@
- it is a <= edge and no parallel < edge was found earlier
- it is a < edge
*)
- fun insert (h,l) [] = [(h,l)]
+ fun insert (h: int,l) [] = [(h,l)]
| insert (h,l) ((k',l')::es) = if h = k' then (
case l of (Less (_, _, _)) => (h,l)::es
| _ => (case l' of (Less (_, _, _)) => (h,l')::es
--- a/src/Pure/Isar/attrib.ML Thu Jul 05 00:06:13 2007 +0200
+++ b/src/Pure/Isar/attrib.ML Thu Jul 05 00:06:14 2007 +0200
@@ -54,7 +54,7 @@
val empty = NameSpace.empty_table;
val copy = I;
val extend = I;
- fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
+ fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
error ("Attempt to merge different versions of attribute(s) " ^ commas_quote dups);
);
--- a/src/Pure/Isar/method.ML Thu Jul 05 00:06:13 2007 +0200
+++ b/src/Pure/Isar/method.ML Thu Jul 05 00:06:14 2007 +0200
@@ -389,7 +389,7 @@
val empty = NameSpace.empty_table;
val copy = I;
val extend = I;
- fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
+ fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
error ("Attempt to merge different versions of method(s) " ^ commas_quote dups);
);
--- a/src/Pure/Thy/term_style.ML Thu Jul 05 00:06:13 2007 +0200
+++ b/src/Pure/Thy/term_style.ML Thu Jul 05 00:06:14 2007 +0200
@@ -27,7 +27,7 @@
val empty = Symtab.empty;
val copy = I;
val extend = I;
- fun merge _ tabs = Symtab.merge (eq_snd (op =)) tabs
+ fun merge _ tabs : T = Symtab.merge (eq_snd (op =)) tabs
handle Symtab.DUPS dups => err_dup_styles dups;
);