--- a/Nominal/NewParser.thy	Thu May 13 07:41:18 2010 +0200
+++ b/Nominal/NewParser.thy	Thu May 13 10:34:59 2010 +0100
@@ -188,7 +188,7 @@
 ML {* print_depth 50 *}
 
 ML {*
-fun prep_bn dt_names dts eqs = 
+fun prep_bn lthy dt_names dts eqs = 
 let
   fun aux eq = 
   let
@@ -205,6 +205,22 @@
     val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements
   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
@@ -219,8 +235,12 @@
   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)
+
+  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 ("ordered'\n" ^ @{make_string} ordered')
 in
-  ordered'
+  ordered' (*map aux2 eqs*)
 end
 *}
 
@@ -254,7 +274,7 @@
    
   val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds 
 
-  val raw_bns = prep_bn 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)
 in
   lthy 
   |> add_datatype_wrapper raw_dt_names raw_dts