--- 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) =