diff -r 02eb0f600630 -r a7e7ffb7f362 Nominal/Parser.thy
--- 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