src/Pure/pattern.ML
changeset 14861 ca5cae7fb65a
parent 14787 724ce6e574e3
child 14875 c48d086264c4
     1.1 --- a/src/Pure/pattern.ML	Tue Jun 01 15:00:26 2004 +0200
     1.2 +++ b/src/Pure/pattern.ML	Tue Jun 01 15:02:05 2004 +0200
     1.3 @@ -114,7 +114,7 @@
     1.4            | mpb _ atom           = atom
     1.5      in mpb 0 end;
     1.6  
     1.7 -fun idx [] j     = ~10000
     1.8 +fun idx [] j     = raise Unif
     1.9    | idx(i::is) j = if i=j then length is else idx is j;
    1.10  
    1.11  fun at xs i = nth_elem (i,xs);
    1.12 @@ -162,7 +162,7 @@
    1.13  
    1.14  (* mk_proj_list(is) = [ |is| - k | 1 <= k <= |is| and is[k] >= 0 ] *)
    1.15  fun mk_proj_list is =
    1.16 -    let fun mk(i::is,j) = if i >= 0 then j :: mk(is,j-1) else mk(is,j-1)
    1.17 +    let fun mk(i::is,j) = if is_some i then j :: mk(is,j-1) else mk(is,j-1)
    1.18            | mk([],_)    = []
    1.19      in mk(is,length is - 1) end;
    1.20  
    1.21 @@ -180,15 +180,13 @@
    1.22                           in (list_comb(f,ts'),env') end
    1.23                   | (Bound(i),ts) =>
    1.24                           let val j = trans d i
    1.25 -                         in if j < 0 then raise Unif
    1.26 -                            else let val (ts',env') = prs(ts,env,d,binders)
    1.27 -                                 in (list_comb(Bound j,ts'),env') end
    1.28 -                         end
    1.29 +                             val (ts',env') = prs(ts,env,d,binders)
    1.30 +                         in (list_comb(Bound j,ts'),env') end
    1.31                   | (Var(F as (a,_),Fty),ts) =>
    1.32                        let val js = ints_of' env ts;
    1.33 -                          val js' = map (trans d) js;
    1.34 +                          val js' = map (try (trans d)) js;
    1.35                            val ks = mk_proj_list js';
    1.36 -                          val ls = filter (fn i => i >= 0) js'
    1.37 +                          val ls = mapfilter I js'
    1.38                            val Hty = type_of_G env (Fty,length js,ks)
    1.39                            val (env',H) = Envir.genvar a (env,Hty)
    1.40                            val env'' =