src/Pure/pattern.ML
changeset 2227 18e993700540
parent 1576 af8f43f742a0
child 2616 704b6c7432cf
equal deleted inserted replaced
2226:f3c6a22681b1 2227:18e993700540
    54           | mpb _ atom           = atom
    54           | mpb _ atom           = atom
    55     in mpb 0 end;
    55     in mpb 0 end;
    56 
    56 
    57 fun idx [] j     = ~10000
    57 fun idx [] j     = ~10000
    58   | idx(i::is) j = if i=j then length is else idx is j;
    58   | idx(i::is) j = if i=j then length is else idx is j;
    59 
       
    60 val nth_type = snd o nth_elem;
       
    61 
    59 
    62 fun at xs i = nth_elem (i,xs);
    60 fun at xs i = nth_elem (i,xs);
    63 
    61 
    64 fun mkabs (binders,is,t)  =
    62 fun mkabs (binders,is,t)  =
    65     let fun mk(i::is) = let val (x,T) = nth_elem(i,binders)
    63     let fun mk(i::is) = let val (x,T) = nth_elem(i,binders)