src/Pure/pattern.ML
changeset 1576 af8f43f742a0
parent 1501 bb7f99a0a6f0
child 2227 18e993700540
     1.1 --- a/src/Pure/pattern.ML	Wed Mar 13 11:56:15 1996 +0100
     1.2 +++ b/src/Pure/pattern.ML	Thu Mar 14 10:40:21 1996 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4  fun ints_of []             = []
     1.5    | ints_of (Bound i ::bs) = 
     1.6        let val is = ints_of bs
     1.7 -      in if i mem is then raise Pattern else i::is end
     1.8 +      in if i mem_int is then raise Pattern else i::is end
     1.9    | ints_of _              = raise Pattern;
    1.10  
    1.11  
    1.12 @@ -167,10 +167,10 @@
    1.13  
    1.14  fun flexflex2(env,binders,F,Fty,is,G,Gty,js) =
    1.15    let fun ff(F,Fty,is,G as (a,_),Gty,js) =
    1.16 -            if js subset is
    1.17 +            if js subset_int is
    1.18              then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
    1.19                   in Envir.update((F,t),env) end
    1.20 -            else let val ks = is inter js
    1.21 +            else let val ks = is inter_int js
    1.22                       val Hty = type_of_G(Fty,length is,map (idx is) ks)
    1.23                       val (env',H) = Envir.genvar a (env,Hty)
    1.24                       fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
    1.25 @@ -227,7 +227,7 @@
    1.26  fun eta_contract (Abs(a,T,body)) = 
    1.27        (case eta_contract body  of
    1.28          body' as (f $ Bound i) => 
    1.29 -	  if i=0 andalso not (0 mem loose_bnos f) then incr_boundvars ~1 f 
    1.30 +	  if i=0 andalso not (0 mem_int loose_bnos f) then incr_boundvars ~1 f 
    1.31  	  else Abs(a,T,body')
    1.32        | body' => Abs(a,T,body'))
    1.33    | eta_contract(f$t) = eta_contract f $ eta_contract t
    1.34 @@ -249,7 +249,7 @@
    1.35        fun mtch (tyinsts,insts) = fn
    1.36  	(Var(ixn,T), t)  =>
    1.37  	  if loose_bvar(t,0) then raise MATCH
    1.38 -	  else (case assoc(insts,ixn) of
    1.39 +	  else (case assoc_string_int(insts,ixn) of
    1.40  		  None => (typ_match (tyinsts, (T, fastype_of t)), 
    1.41  			   (ixn,t)::insts)
    1.42  		| Some u => if t aconv u then (tyinsts,insts) else raise MATCH)
    1.43 @@ -270,7 +270,7 @@
    1.44    let val js = loose_bnos t
    1.45    in if null is
    1.46       then if null js then (ixn,t)::itms else raise MATCH
    1.47 -     else if js subset is
    1.48 +     else if js subset_int is
    1.49            then let val t' = if downto0(is,length binders - 1) then t
    1.50                              else mapbnd (idx is) t
    1.51                 in (ixn, mkabs(binders,is,t')) :: itms end
    1.52 @@ -320,7 +320,7 @@
    1.53        in case ph of
    1.54             Var(ixn,_) =>
    1.55               let val is = ints_of pargs
    1.56 -             in case assoc(itms,ixn) of
    1.57 +             in case assoc_string_int(itms,ixn) of
    1.58                    None => (iTs,match_bind(itms,binders,ixn,is,obj))
    1.59                  | Some u => if obj aeconv (red u is []) then env
    1.60                              else raise MATCH