src/Pure/pattern.ML
changeset 16668 fdb4992cf1d2
parent 16651 40b96a501773
child 16939 87fc64d2409f
--- 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) =>