diff -r f3c6a22681b1 -r 18e993700540 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Tue Nov 26 16:11:18 1996 +0100
+++ b/src/Pure/pattern.ML	Tue Nov 26 16:15:50 1996 +0100
@@ -57,8 +57,6 @@
 fun idx [] j     = ~10000
   | idx(i::is) j = if i=j then length is else idx is j;
 
-val nth_type = snd o nth_elem;
-
 fun at xs i = nth_elem (i,xs);
 
 fun mkabs (binders,is,t)  =