diff -r ad03df7e8056 -r 25d2cdf7d7e4 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Mon Jun 07 11:46:26 2010 +0200
+++ b/Nominal-General/nominal_library.ML	Wed Jun 09 15:14:16 2010 +0200
@@ -6,6 +6,8 @@
 
 signature NOMINAL_LIBRARY =
 sig
+  val last2: 'a list -> 'a * 'a
+
   val dest_listT: typ -> typ
 
   val mk_minus: term -> term
@@ -57,7 +59,11 @@
 structure Nominal_Library: NOMINAL_LIBRARY =
 struct
 
-(* this function should be in hologic.ML *)
+fun last2 [] = raise Empty
+  | last2 [_] = raise Empty
+  | last2 [x, y] = (x,y)
+  | last2 (_ :: xs) = last2 xs
+
 fun dest_listT (Type (@{type_name list}, [T])) = T
   | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])