# HG changeset patch
# User wenzelm
# Date 1183586774 -7200
# Node ID c5b93c69afd3833b05f30404ac33dbdb9ec67300
# Parent  1ffe739e5ee0b544d2b33c1f8dc20b24d07c0a9f
avoid polymorphic equality;

diff -r 1ffe739e5ee0 -r c5b93c69afd3 src/HOL/Tools/datatype_realizer.ML
--- 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;
diff -r 1ffe739e5ee0 -r c5b93c69afd3 src/HOL/Tools/inductive_package.ML
--- 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 =
diff -r 1ffe739e5ee0 -r c5b93c69afd3 src/HOL/Tools/inductive_realizer.ML
--- 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 =
diff -r 1ffe739e5ee0 -r c5b93c69afd3 src/Provers/Arith/fast_lin_arith.ML
--- 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;
 
diff -r 1ffe739e5ee0 -r c5b93c69afd3 src/Provers/order.ML
--- 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
diff -r 1ffe739e5ee0 -r c5b93c69afd3 src/Pure/Isar/attrib.ML
--- 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);
 );
 
diff -r 1ffe739e5ee0 -r c5b93c69afd3 src/Pure/Isar/method.ML
--- 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);
 );
 
diff -r 1ffe739e5ee0 -r c5b93c69afd3 src/Pure/Thy/term_style.ML
--- 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;
 );