--- a/Nominal/Parser.thy	Mon Mar 01 16:55:41 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 01 19:23:08 2010 +0100
@@ -4,7 +4,6 @@
 
 atom_decl name
 
-
 section{* Interface for nominal_datatype *}
 
 text {*
@@ -108,14 +107,14 @@
 
 ML {*
 fun get_cnstrs dts =
-  flat (map (fn (_, _, _, constrs) => constrs) dts)
+  map (fn (_, _, _, constrs) => constrs) dts
 
 fun get_typed_cnstrs dts =
   flat (map (fn (_, bn, _, constrs) => 
    (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts)
 
 fun get_cnstr_strs dts =
-  map (fn (bn, _, _) => Binding.name_of bn) (get_cnstrs dts)
+  map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts))
 
 fun get_bn_fun_strs bn_funs =
   map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs
@@ -246,14 +245,12 @@
 *}
 
 ML {*
-fun forth (_, _, _, x) = x
-
-fun find_all eq xs k' = 
-  maps (fn (k, v) => if eq (k, k') then [v] else []) xs
+fun find_all eq xs (k',i) = 
+  maps (fn (k, (v1, v2)) => if eq (k, k') then [(v1, v2, i)] else []) xs
 *}
 
 ML {*
-(* associates every SOME with the index in the list *)
+(* associates every SOME with the index in the list; drops NONEs *)
 fun mk_env xs =
   let
     fun mapp (_: int) [] = []
@@ -271,37 +268,35 @@
   | NONE => error ("cannot find " ^ x ^ " in the binding specification.");
 *}
 
-
-
 ML {*
 fun prepare_binds dt_strs lthy = 
 let
   fun extract_annos_binds dt_strs =
-    map ((map (fn (_, antys, _, bns) => (map fst antys, bns))) o forth) dt_strs
+    map (map (fn (_, antys, _, bns) => (map fst antys, bns))) dt_strs
 
   fun prep_bn env bn_str =
     case (Syntax.read_term lthy bn_str) of
-       Free (x, _) => (env_lookup env x, NONE)
-     | Const (a, T) $ Free (x, _) => (env_lookup env x, SOME (Const (a, T)))
+       Free (x, _) => (NONE, env_lookup env x)
+     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), env_lookup env x)
      | _ => error (bn_str ^ " not allowed as binding specification.");  
  
-  fun prep_typ env opt_name = 
+  fun prep_typ env (i, opt_name) = 
     case opt_name of
       NONE => []
-    | SOME x => find_all (op=) env x;
+    | SOME x => find_all (op=) env (x,i);
         
   (* annos - list of annotation for each type (either NONE or SOME fo a type *)
   
   fun prep_binds (annos, bind_strs) = 
   let
-    val env = mk_env annos (* for ever label the index *)
+    val env = mk_env annos (* for every label the index *)
     val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs  
   in
-    map (prep_typ binds) annos
+    map_index (prep_typ binds) annos
   end
 
 in
-  map (map prep_binds) (extract_annos_binds dt_strs)
+  map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))
 end
 *}
 
@@ -317,7 +312,7 @@
     ||>> prepare_bn_funs bn_fun_strs bn_eq_strs
     ||> prepare_binds dt_strs
   
-  (*val _ = tracing (PolyML.makestring binds)*)
+  val _ = tracing (PolyML.makestring binds)
 in
   nominal_datatype2 dts bn_fun bn_eq binds lthy |> snd
 end

--- a/Nominal/Test.thy	Mon Mar 01 16:55:41 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 01 19:23:08 2010 +0100
@@ -40,7 +40,7 @@
 where 
   "f PN = {}"
 | "f (PS x) = {x}"
-| "f (PD x y) = {x,y}"
+| "f (PD x y) = {x, y}"
 
 thm f_raw.simps
 
@@ -78,7 +78,7 @@
 nominal_datatype trm1 =
   Vr1 "name"
 | Ap1 "trm1" "trm1"
-| Lm1 x::"name" t::"trm1"      bind x in t 
+| Lm1 x::"name" t::"trm1"       bind x in t 
 | Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t 
 and bp1 =
   BUnit1
@@ -203,13 +203,13 @@
 atom_decl coname
 
 nominal_datatype phd =
-   Ax name coname
-|  Cut n::name t1::phd c::coname t2::phd               bind n in t1, bind c in t2
-|  AndR c1::coname t1::phd c2::coname t2::phd coname   bind c1 in t1, bind c2 in t2
-|  AndL1 n::name t::phd name                           bind n in t
-|  AndL2 n::name t::phd name                           bind n in t
-|  ImpL c::coname t1::phd n::name t2::phd name         bind c in t1, bind n in t2
-|  ImpR c::coname n::name t::phd coname                bind n in 1, bind c in t
+   Ax "name" "coname"
+|  Cut n::"coname" t1::"phd" c::"coname" t2::"phd"              bind n in t1, bind c in t2
+|  AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname"  bind c1 in t1, bind c2 in t2
+|  AndL1 n::"name" t::"phd" "name"                              bind n in t
+|  AndL2 n::"name" t::"phd" "name"                              bind n in t
+|  ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name"        bind c in t1, bind n in t2
+|  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in 1, bind c in t
 
 (* example form Leroy 96 about modules; OTT *)