--- a/Nominal/Parser.thy	Tue Mar 09 22:10:10 2010 +0100
+++ b/Nominal/Parser.thy	Wed Mar 10 12:48:38 2010 +0100
@@ -150,7 +150,12 @@
 *}
 
 ML {*
-fun prep_bn dt_names eqs lthy = 
+fun find [] _ = error ("cannot find element")
+  | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y
+*}
+
+ML {*
+fun prep_bn dt_names dts eqs lthy = 
 let
   fun aux eq = 
   let
@@ -158,17 +163,30 @@
       |> strip_qnt_body "all" 
       |> HOLogic.dest_Trueprop
       |> HOLogic.dest_eq
-    val (head, [cnstr]) = strip_comb lhs
-    val (_, ty) = dest_Free head
+    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_args) = strip_comb cnstr
+    val (cnstr_head, cnstr_args) = strip_comb cnstr
     val included = map (fn i => length (cnstr_args) - i - 1) (loose_bnos rhs)
   in
-    (head, dt_index, included)
-  end  
+    (dt_index, (bn_fun, (cnstr_head, included)))
+  end 
+ 
+  fun order dts i ts = 
+  let
+    val dt = nth dts i
+    val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt)
+    val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts
+  in
+    map (find ts') cts
+  end
+
+  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' 
 in
-  map aux eqs
+  ordered
 end
 *}
 
@@ -223,7 +241,7 @@
   
   val raw_binds = rawify_binds dts_env cnstrs_env bn_fun_full_env binds 
 
-  val raw_bns = prep_bn dt_full_names' (map snd raw_bn_eqs) lthy
+  val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs) lthy
 
   val _ = tracing (cat_lines (map PolyML.makestring raw_bns)) 
 in

--- a/Nominal/Test.thy	Tue Mar 09 22:10:10 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 10 12:48:38 2010 +0100
@@ -141,8 +141,9 @@
   bv1
 where
   "bv1 (BUnit1) = {}"
+| "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 | "bv1 (BV1 x) = {atom x}"
-| "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
+
 
 thm bv1_raw.simps
 
@@ -338,12 +339,13 @@
   "cbinders (Type t T) = {atom t}"
 | "cbinders (Dty t) = {atom t}"
 | "cbinders (DStru x s) = {atom x}"
-| "cbinders (Val v M) = {atom v}"
+| "cbinders (Val v M) = {atom v}"*)
 | "Cbinders (Type1 t) = {atom t}"
 | "Cbinders (Type2 t T) = {atom t}"
 | "Cbinders (SStru x S) = {atom x}"
 | "Cbinders (SVal v T) = {atom v}"  
 
+
 (* core haskell *)
 print_theorems