--- a/Nominal/NewParser.thy	Sun May 16 11:00:44 2010 +0100
+++ b/Nominal/NewParser.thy	Sun May 16 12:41:27 2010 +0100
@@ -204,22 +204,6 @@
   in
     (dt_index, (bn_fun, (cnstr_head, included)))
   end
-  fun aux2 eq = 
-  let
-    val (lhs, rhs) = eq
-      |> strip_qnt_body "all" 
-      |> HOLogic.dest_Trueprop
-      |> HOLogic.dest_eq
-    val (bn_fun, [cnstr]) = strip_comb lhs
-    val (_, ty) = dest_Free bn_fun
-    val (ty_name, _) = dest_Type (domain_type ty)
-    val dt_index = find_index (fn x => x = ty_name) dt_names
-    val (cnstr_head, cnstr_args) = strip_comb cnstr
-    val rhs_elements = strip_bn_fun rhs
-    val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements
-  in
-    (bn_fun, dt_index, (cnstr_head, included))
-  end 
   fun order dts i ts = 
   let
     val dt = nth dts i
@@ -235,13 +219,14 @@
   val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered)
 
   val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))
-  val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))
+  (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*)
   val _ = tracing ("ordered'\n" ^ @{make_string} ordered')
 in
   ordered'
 end
 *}
 
+ML {* add_primrec_wrapper *}
 ML {*
 fun raw_nominal_decls dts bn_funs bn_eqs binds lthy =
 let
@@ -271,14 +256,16 @@
   val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs 
    
   val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds 
+  val raw_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs)
 
-  val raw_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs)
+  val (raw_dt_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy
+  val ((raw_bn_funs, raw_bn_eqs), lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1
+
+  val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
+  fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l);
+  val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns;
 in
-  lthy 
-  |> add_datatype_wrapper raw_dt_names raw_dts 
-  ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs
-  ||>> pair raw_bclauses
-  ||>> pair raw_bns
+  (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, lthy2)
 end
 *}
 
@@ -388,7 +375,7 @@
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
   (* definition of the raw datatype and raw bn-functions *)
-  val ((((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_bclauses), raw_bns), lthy1) =
+  val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, lthy1) =
     if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
@@ -413,32 +400,25 @@
     then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1
     else raise TEST lthy1
 
-  (* definition of raw fv_functions *)
-  val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
-  fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l);
-  val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns;
- 
   val (_, lthy2a) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2;
   val thy = Local_Theory.exit_global lthy2a;
   val thy_name = Context.theory_name thy
 
+  (* definition of raw fv_functions *)
   val lthy3 = Theory_Target.init NONE thy;
-  val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls;
+  val raw_bn_funs = map (fn (f, _, _) => f) raw_bns;
 
-  val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns)
-  val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls)
-   
   val ((fv, fvbn), fv_def, lthy3a) = 
     if get_STEPS lthy > 3 
-    then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3
+    then define_raw_fv descr sorts raw_bns raw_bclauses lthy3
     else raise TEST lthy3
   
 
   (* definition of raw alphas *)
   val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
     if get_STEPS lthy > 4 
-    then define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a
+    then define_raw_alpha dtinfo raw_bns raw_bclauses fv lthy3a
     else raise TEST lthy3a
   
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts