# HG changeset patch
# User paulson
# Date 849021350 -3600
# Node ID 18e993700540f34fec2c8b9dbf0d66a72ec2a48c
# Parent  f3c6a22681b1399e55c98bb1d5422604eb832347
Removal of needless function definition

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