--- a/Nominal/Nominal2.thy	Thu Jul 07 16:17:03 2011 +0200
+++ b/Nominal/Nominal2.thy	Fri Jul 08 05:04:23 2011 +0200
@@ -215,6 +215,27 @@
 end
 *}
 
+ML {*
+infix 1 ||>>> |>>>
+
+fun (x |>>> f) = 
+  let 
+    val (x', y') = f x 
+  in
+    ([x'], y')
+  end
+
+fun (([], y) ||>>> f) = ([], y)  
+  | ((xs, y) ||>>> f) =
+       let
+         val (x', y') = f y
+       in
+         (xs @ [x'], y')
+       end;
+(op ||>>)
+*}
+
+
 
 ML {*
 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy =
@@ -243,7 +264,7 @@
   val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = define_raw_perms raw_dt_info lthy0
  
   (* noting the raw permutations as eqvt theorems *)
-  val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a
+  val lthy3 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a)
 
   val _ = trace_msg (K "Defining raw fv- and bn-functions...")
   val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_inducts, lthy3a) =
@@ -406,31 +427,28 @@
   val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def
     prod.cases} 
 
-  val (((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), qbn_inducts), 
-    lthyA) = 
+  val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, 
+         qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps, 
+         qalpha_refl_thms ], lthyB) = 
     lthy9a    
-    |> lift_thms qtys [] alpha_distincts  
-    ||>> lift_thms qtys eq_iff_simps alpha_eq_iff       
-    ||>> lift_thms qtys [] raw_fv_defs
-    ||>> lift_thms qtys [] raw_bn_defs
-    ||>> lift_thms qtys [] raw_perm_simps
-    ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt)
-    ||>> lift_thms qtys [] raw_bn_inducts
-
-  val ((((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), qalpha_refl_thms), lthyB) = 
-    lthyA 
-    |> lift_thms qtys [] raw_size_eqvt
-    ||>> lift_thms qtys [] [raw_induct_thm]
-    ||>> lift_thms qtys [] raw_exhaust_thms
-    ||>> lift_thms qtys [] raw_size_thms
-    ||>> lift_thms qtys [] raw_perm_bn_simps
-    ||>> lift_thms qtys [] alpha_refl_thms
+    |>>> lift_thms qtys [] alpha_distincts  
+    ||>>> lift_thms qtys eq_iff_simps alpha_eq_iff       
+    ||>>> lift_thms qtys [] raw_fv_defs
+    ||>>> lift_thms qtys [] raw_bn_defs
+    ||>>> lift_thms qtys [] raw_perm_simps
+    ||>>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt)
+    ||>>> lift_thms qtys [] raw_bn_inducts
+    ||>>> lift_thms qtys [] raw_size_eqvt
+    ||>>> lift_thms qtys [] [raw_induct_thm]
+    ||>>> lift_thms qtys [] raw_exhaust_thms
+    ||>>> lift_thms qtys [] raw_size_thms
+    ||>>> lift_thms qtys [] raw_perm_bn_simps
+    ||>>> lift_thms qtys [] alpha_refl_thms
 
   val qinducts = Project_Rule.projections lthyB qinduct
 
   val _ = trace_msg (K "Proving supp lemmas and fs-instances...")
-  val qsupports_thms =
-    prove_supports lthyB qperm_simps (flat qtrms)
+  val qsupports_thms = prove_supports lthyB qperm_simps (flat qtrms)
 
   (* finite supp lemmas *)
   val qfsupp_thms = prove_fsupp lthyB qtys qinduct qsupports_thms
@@ -551,6 +569,7 @@
   
   fun prep_dts (tvs, tname, mx, constrs) (constr_trms, dts, sorts) =
   let 
+
     val (constrs', sorts') = 
       fold prep_constr constrs ([], sorts)
 

--- a/Nominal/nominal_basics.ML	Thu Jul 07 16:17:03 2011 +0200
+++ b/Nominal/nominal_basics.ML	Fri Jul 08 05:04:23 2011 +0200
@@ -10,6 +10,7 @@
   val trace_msg: (unit -> string) -> unit
 
   val last2: 'a list -> 'a * 'a
+  val split_triples: ('a * 'b * 'c) list -> ('a list * 'b list * 'c list)
   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
@@ -68,6 +69,9 @@
       then remove_dups eq xs 
       else x :: remove_dups eq xs
 
+fun split_triples xs =
+  fold (fn (a, b, c) => fn (axs, bxs, cxs) => (a :: axs, b :: bxs, c :: cxs)) xs ([], [], [])
+
 fun last2 [] = raise Empty
   | last2 [_] = raise Empty
   | last2 [x, y] = (x, y)

--- a/Nominal/nominal_dt_data.ML	Thu Jul 07 16:17:03 2011 +0200
+++ b/Nominal/nominal_dt_data.ML	Fri Jul 08 05:04:23 2011 +0200
@@ -27,6 +27,14 @@
   val register_info: (string * info) -> Context.generic -> Context.generic
   val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list
 
+  datatype user_data = UserData of
+    {dts      : dt_info,
+     cn_names : string list,
+     cn_tys   : (string * string) list,
+     bn_funs  : (binding * typ * mixfix) list,
+     bn_eqs   : (Attrib.binding * term) list,
+     bclauses : bclause list list list}
+
   datatype raw_dt_info = RawDtInfo of
     {raw_dt_names         : string list,
      raw_dts              : dt_info,
@@ -112,6 +120,14 @@
 end
 
 
+datatype user_data = UserData of
+  {dts      : dt_info,
+   cn_names : string list,
+   cn_tys   : (string * string) list,
+   bn_funs  : (binding * typ * mixfix) list,
+   bn_eqs   : (Attrib.binding * term) list,
+   bclauses : bclause list list list}
+
 datatype raw_dt_info = RawDtInfo of
   {raw_dt_names         : string list,
    raw_dts              : dt_info,