avoid polyeq;

--- a/src/Pure/Isar/proof_context.ML	Fri Jul 01 22:35:20 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Jul 01 22:35:41 2005 +0200
@@ -1220,7 +1220,7 @@
     else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt)
   end;
 
-fun rem_case name = remove (fn (x, (y, _)) => x = y) name;
+fun rem_case name = remove (fn (x: string, (y, _)) => x = y) name;
 
 fun add_case ("", _) cases = cases
   | add_case (name, NONE) cases = rem_case name cases

--- a/src/Pure/Syntax/parser.ML	Fri Jul 01 22:35:20 2005 +0200
+++ b/src/Pure/Syntax/parser.ML	Fri Jul 01 22:35:41 2005 +0200
@@ -627,7 +627,7 @@
 
 (*Add parse tree to list and eliminate duplicates
   saving the maximum precedence*)
-fun conc (t, prec:int) [] = (NONE, [(t, prec)])
+fun conc (t: parsetree list, prec:int) [] = (NONE, [(t, prec)])
   | conc (t, prec) ((t', prec') :: ts) =
       if t = t' then
         (SOME prec', if prec' >= prec then (t', prec') :: ts
@@ -637,7 +637,7 @@
         in (n, (t', prec') :: ts') end;
 
 (*Update entry in used*)
-fun update_trees ((B, (i, ts)) :: used) (A, t) =
+fun update_trees ((B: nt_tag, (i, ts)) :: used) (A, t) =
   if A = B then
     let val (n, ts') = conc t ts
     in ((A, (i, ts')) :: used, n) end
@@ -646,7 +646,7 @@
     in ((B, (i, ts)) :: used', n) end;
 
 (*Replace entry in used*)
-fun update_prec (A, prec) used =
+fun update_prec (A: nt_tag, prec) used =
   let fun update ((hd as (B, (_, ts))) :: used, used') =
         if A = B
         then used' @ ((A, (prec, ts)) :: used)

--- a/src/Pure/pattern.ML	Fri Jul 01 22:35:20 2005 +0200
+++ b/src/Pure/pattern.ML	Fri Jul 01 22:35:41 2005 +0200
@@ -111,7 +111,7 @@
     in mpb 0 end;
 
 fun idx [] j     = raise Unif
-  | idx(i::is) j = if i=j then length is else idx is j;
+  | idx(i::is) j = if (i:int) =j then length is else idx is j;
 
 fun at xs i = List.nth (xs,i);
 
@@ -202,7 +202,7 @@
 (* mk_ff_list(is,js) = [ length(is) - k | 1 <= k <= |is| and is[k] = js[k] ] *)
 fun mk_ff_list(is,js) =
     let fun mk([],[],_)        = []
-          | mk(i::is,j::js, k) = if i=j then k :: mk(is,js,k-1)
+          | mk(i::is,j::js, k) = if (i:int) = j then k :: mk(is,js,k-1)
                                         else mk(is,js,k-1)
           | mk _               = error"mk_ff_list"
     in mk(is,js,length is-1) end;
@@ -408,8 +408,8 @@
     let val (ph,pargs) = strip_comb pat
         fun rigrig1(iTs,oargs) =
               Library.foldl (mtch binders) ((iTs,itms), pargs~~oargs)
-        fun rigrig2((a,Ta),(b,Tb),oargs) =
-              if a<> b then raise MATCH
+        fun rigrig2((a:string,Ta),(b,Tb),oargs) =
+              if a <> b then raise MATCH
               else rigrig1(typ_match tsg (iTs,(Ta,Tb)), oargs)
     in case ph of
          Var(ixn,T) =>

--- a/src/Pure/type_infer.ML	Fri Jul 01 22:35:20 2005 +0200
+++ b/src/Pure/type_infer.ML	Fri Jul 01 22:35:41 2005 +0200
@@ -448,7 +448,7 @@
 
 fun get_sort tsig def_sort map_sort raw_env =
   let
-    fun eq ((xi, S), (xi', S')) =
+    fun eq ((xi: indexname, S), (xi', S')) =
       xi = xi' andalso Type.eq_sort tsig (S, S');
 
     val env = gen_distinct eq (map (apsnd map_sort) raw_env);