diff -r 98236fbd8aa6 -r 25dcb2b1329e Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/nominal_library.ML	Mon Dec 06 14:24:17 2010 +0000
@@ -6,11 +6,14 @@
 
 signature NOMINAL_LIBRARY =
 sig
-  val is_true: term -> bool
+  val last2: 'a list -> 'a * 'a
+  val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
 
-  val last2: 'a list -> 'a * 'a
+  val is_true: term -> bool
+ 
+  val dest_listT: typ -> typ
 
-  val dest_listT: typ -> typ
+  val mk_id: term -> term
 
   val size_const: typ -> term 
 
@@ -91,17 +94,30 @@
 structure Nominal_Library: NOMINAL_LIBRARY =
 struct
 
-fun is_true @{term "Trueprop True"} = true
-  | is_true _ = false 
+(* orders an AList according to keys *)
+fun order eq keys list = 
+  map (the o AList.lookup eq list) keys
 
 fun last2 [] = raise Empty
   | last2 [_] = raise Empty
   | last2 [x, y] = (x, y)
   | last2 (_ :: xs) = last2 xs
 
+
+fun is_true @{term "Trueprop True"} = true
+  | is_true _ = false 
+
 fun dest_listT (Type (@{type_name list}, [T])) = T
   | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
 
+fun mk_id trm =
+  let 
+    val ty = fastype_of trm
+  in
+    Const (@{const_name id}, ty --> ty) $ trm
+  end
+
+
 fun size_const ty = Const (@{const_name size}, ty --> @{typ nat})
 
 fun sum_case_const ty1 ty2 ty3 =