src/Pure/pattern.ML
changeset 16668 fdb4992cf1d2
parent 16651 40b96a501773
child 16939 87fc64d2409f
     1.1 --- a/src/Pure/pattern.ML	Fri Jul 01 22:35:20 2005 +0200
     1.2 +++ b/src/Pure/pattern.ML	Fri Jul 01 22:35:41 2005 +0200
     1.3 @@ -111,7 +111,7 @@
     1.4      in mpb 0 end;
     1.5  
     1.6  fun idx [] j     = raise Unif
     1.7 -  | idx(i::is) j = if i=j then length is else idx is j;
     1.8 +  | idx(i::is) j = if (i:int) =j then length is else idx is j;
     1.9  
    1.10  fun at xs i = List.nth (xs,i);
    1.11  
    1.12 @@ -202,7 +202,7 @@
    1.13  (* mk_ff_list(is,js) = [ length(is) - k | 1 <= k <= |is| and is[k] = js[k] ] *)
    1.14  fun mk_ff_list(is,js) =
    1.15      let fun mk([],[],_)        = []
    1.16 -          | mk(i::is,j::js, k) = if i=j then k :: mk(is,js,k-1)
    1.17 +          | mk(i::is,j::js, k) = if (i:int) = j then k :: mk(is,js,k-1)
    1.18                                          else mk(is,js,k-1)
    1.19            | mk _               = error"mk_ff_list"
    1.20      in mk(is,js,length is-1) end;
    1.21 @@ -408,8 +408,8 @@
    1.22      let val (ph,pargs) = strip_comb pat
    1.23          fun rigrig1(iTs,oargs) =
    1.24                Library.foldl (mtch binders) ((iTs,itms), pargs~~oargs)
    1.25 -        fun rigrig2((a,Ta),(b,Tb),oargs) =
    1.26 -              if a<> b then raise MATCH
    1.27 +        fun rigrig2((a:string,Ta),(b,Tb),oargs) =
    1.28 +              if a <> b then raise MATCH
    1.29                else rigrig1(typ_match tsg (iTs,(Ta,Tb)), oargs)
    1.30      in case ph of
    1.31           Var(ixn,T) =>