--- a/Nominal/Nominal2_Abs.thy	Fri Dec 31 15:37:04 2010 +0000
+++ b/Nominal/Nominal2_Abs.thy	Mon Jan 03 16:19:27 2011 +0000
@@ -1,9 +1,9 @@
 theory Nominal2_Abs
 imports "Nominal2_Base" 
         "Nominal2_Eqvt" 
-        "Quotient" 
-        "Quotient_List"
-        "Quotient_Product" 
+        "~~/src/HOL/Quotient" 
+        "~~/src/HOL/Library/Quotient_List"
+        "~~/src/HOL/Library/Quotient_Product" 
 begin
 
 

--- a/Nominal/Nominal2_Base.thy	Fri Dec 31 15:37:04 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Mon Jan 03 16:19:27 2011 +0000
@@ -5,7 +5,8 @@
     Nominal Isabelle. 
 *)
 theory Nominal2_Base
-imports Main Infinite_Set
+imports Main 
+        "~~/src/HOL/Library/Infinite_Set"
         "~~/src/HOL/Quotient_Examples/FSet"
 uses ("nominal_library.ML")
      ("nominal_atoms.ML")
@@ -687,6 +688,7 @@
 instance bool :: pure
 proof qed (rule permute_bool_def)
 
+
 text {* Other type constructors preserve purity. *}
 
 instance "fun" :: (pure, pure) pure

--- a/Nominal/Nominal2_Eqvt.thy	Fri Dec 31 15:37:04 2010 +0000
+++ b/Nominal/Nominal2_Eqvt.thy	Mon Jan 03 16:19:27 2011 +0000
@@ -24,9 +24,9 @@
 section {* eqvt lemmas *}
 
 lemmas [eqvt] =
-  conj_eqvt Not_eqvt ex_eqvt all_eqvt imp_eqvt
+  conj_eqvt Not_eqvt ex_eqvt all_eqvt imp_eqvt uminus_eqvt
   imp_eqvt[folded induct_implies_def]
-  uminus_eqvt
+  all_eqvt[folded induct_forall_def]
 
   (* nominal *)
   supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt 
@@ -41,6 +41,7 @@
   (* fsets *)
   permute_fset fset_eqvt
 
+
 text {* helper lemmas for the perm_simp *}
 
 definition

--- a/Nominal/nominal_dt_quot.ML	Fri Dec 31 15:37:04 2010 +0000
+++ b/Nominal/nominal_dt_quot.ML	Mon Jan 03 16:19:27 2011 +0000
@@ -671,7 +671,7 @@
 
 fun prove_strong_induct lthy induct exhausts size_thms bclausesss =
   let
-    val ((insts, [induct']), lthy') = Variable.import true [induct] lthy
+    val ((_, [induct']), lthy') = Variable.import true [induct] lthy
 
     val ([c_name, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
     val c_ty = TFree (a, @{sort fs})

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