diff -r d0f83a35950e -r 9bd97ed202f7 Nominal/Nominal2.thy
--- 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)