--- a/Nominal/NewParser.thy	Wed May 12 16:26:06 2010 +0100
+++ b/Nominal/NewParser.thy	Wed May 12 16:33:25 2010 +0100
@@ -185,6 +185,8 @@
   | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y
 *}
 
+ML {* print_depth 50 *}
+
 ML {*
 fun prep_bn dt_names dts eqs = 
 let
@@ -216,8 +218,9 @@
   val unordered = AList.group (op=) (map aux eqs)
   val unordered' = map (fn (x, y) =>  (x, AList.group (op=) y)) unordered
   val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' 
+  val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered)
 in
-  ordered
+  ordered'
 end
 *}
 
@@ -389,10 +392,9 @@
 
   (* definition of raw fv_functions *)
   val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
-  fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
-  val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
-  val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
-
+  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;
@@ -402,10 +404,8 @@
   val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls;
 
   val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns)
-  val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns_exp)
   val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls)
-  val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses)
-  
+   
   val ((fv, fvbn), fv_def, lthy3a) = 
     if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3
     else raise TEST lthy3