--- 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