diff -r 3ce1089cdbf3 -r 64b4cb2c2bf8 Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Fri Dec 31 15:37:04 2010 +0000
+++ b/Nominal/nominal_library.ML	Mon Jan 03 16:19:27 2011 +0000
@@ -7,7 +7,9 @@
 signature NOMINAL_LIBRARY =
 sig
   val last2: 'a list -> 'a * 'a
+  val split_last2: 'a list -> 'a list * 'a * 'a
   val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
+  val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list
   val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list
   val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
   val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list
@@ -20,6 +22,7 @@
 
   val mk_id: term -> term
   val mk_all: (string * typ) -> term -> term
+  val mk_All: (string * typ) -> term -> term
 
   val sum_case_const: typ -> typ -> typ -> term
   val mk_sum_case: term -> term -> term
@@ -28,6 +31,7 @@
   val mk_plus: term -> term -> term
 
   val perm_ty: typ -> typ 
+  val perm_const: typ -> term
   val mk_perm_ty: typ -> term -> term -> term
   val mk_perm: term -> term -> term
   val dest_perm: term -> term * term
@@ -136,10 +140,14 @@
 structure Nominal_Library: NOMINAL_LIBRARY =
 struct
 
-(* orders an AList according to keys *)
+(* orders an AList according to keys - every key needs to be there *)
 fun order eq keys list = 
   map (the o AList.lookup eq list) keys
 
+(* orders an AList according to keys - returns default for non-existing keys *)
+fun order_default eq default keys list = 
+  map (the_default default o AList.lookup eq list) keys
+
 (* remove duplicates *)
 fun remove_dups eq [] = []
   | remove_dups eq (x :: xs) = 
@@ -152,6 +160,14 @@
   | last2 [x, y] = (x, y)
   | last2 (_ :: xs) = last2 xs
 
+fun split_last2 xs = 
+  let
+    val (xs', x) = split_last xs
+    val (xs'', y) = split_last xs'
+  in
+    (xs'', y, x)
+  end
+
 fun map4 _ [] [] [] [] = []
   | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
 
@@ -186,6 +202,8 @@
 
 fun mk_all (a, T) t =  Term.all T $ Abs (a, T, t)
 
+fun mk_All (a, T) t =  HOLogic.all_const T $ Abs (a, T, t)
+
 fun sum_case_const ty1 ty2 ty3 = 
   Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)
 
@@ -204,7 +222,8 @@
 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q
 
 fun perm_ty ty = @{typ "perm"} --> ty --> ty
-fun mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty ty) $ p $ trm
+fun perm_const ty  = Const (@{const_name "permute"}, perm_ty ty)
+fun mk_perm_ty ty p trm = perm_const ty $ p $ trm
 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm
 
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)