Removal of needless function definition
authorpaulson
Tue Nov 26 16:15:50 1996 +0100 (1996-11-26)
changeset 222718e993700540
parent 2226 f3c6a22681b1
child 2228 f381c1a98209
Removal of needless function definition
src/Pure/pattern.ML
     1.1 --- a/src/Pure/pattern.ML	Tue Nov 26 16:11:18 1996 +0100
     1.2 +++ b/src/Pure/pattern.ML	Tue Nov 26 16:15:50 1996 +0100
     1.3 @@ -57,8 +57,6 @@
     1.4  fun idx [] j     = ~10000
     1.5    | idx(i::is) j = if i=j then length is else idx is j;
     1.6  
     1.7 -val nth_type = snd o nth_elem;
     1.8 -
     1.9  fun at xs i = nth_elem (i,xs);
    1.10  
    1.11  fun mkabs (binders,is,t)  =