--- a/Nominal-General/nominal_library.ML	Mon Jul 19 08:55:49 2010 +0100
+++ b/Nominal-General/nominal_library.ML	Tue Jul 20 06:14:16 2010 +0100
@@ -61,7 +61,7 @@
 
 fun last2 [] = raise Empty
   | last2 [_] = raise Empty
-  | last2 [x, y] = (x,y)
+  | last2 [x, y] = (x, y)
   | last2 (_ :: xs) = last2 xs
 
 fun dest_listT (Type (@{type_name list}, [T])) = T

--- a/Nominal/nominal_dt_alpha.ML	Mon Jul 19 08:55:49 2010 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Tue Jul 20 06:14:16 2010 +0100
@@ -65,7 +65,9 @@
     | Set => (mk_union,  bind_set)
     | Res => (mk_union,  bind_set)
 in
-  foldl1 combine_fn (map (bind_fn lthy args) bodies)
+  bodies
+  |> map (bind_fn lthy args)
+  |> foldl1 combine_fn 
 end
 
 (* produces the term for an alpha with abstraction *)

--- a/Nominal/nominal_dt_rawfuns.ML	Mon Jul 19 08:55:49 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Tue Jul 20 06:14:16 2010 +0100
@@ -35,6 +35,11 @@
 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
 struct
 
+(* term              - is constant of the bn-function 
+   int               - is datatype number over which the bn-function is defined
+   int * term option - is number of the corresponding argument with possibly
+                       recursive call with bn-function term 
+*)  
 type bn_info = (term * int * (int * term option) list list) list
 
 datatype bmode = Lst | Res | Set

--- a/Quotient-Paper/Paper.thy	Mon Jul 19 08:55:49 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Tue Jul 20 06:14:16 2010 +0100
@@ -15,6 +15,10 @@
     compositions
   - explain how Quotient R Abs Rep is proved (j-version)
   - give an example where precise specification helps (core Haskell in nominal?)
+
+  - Quote from Peter:
+
+    One might think quotient have been studied to death, but
 *)
 
 notation (latex output)