--- a/Nominal/Parser.thy	Mon Mar 01 11:40:48 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 01 14:26:14 2010 +0100
@@ -126,14 +126,11 @@
 fun raw_dts_decl dt_names dts lthy =
 let
   val thy = ProofContext.theory_of lthy
-  val conf = Datatype.default_config
-
-  val dt_names' = add_raws dt_names
   val dt_full_names = map (Sign.full_bname thy) dt_names 
-  val dts' = raw_dts dt_full_names dts
+  val raw_dts = raw_dts dt_full_names dts
+  val raw_dt_names = add_raws dt_names
 in
-  lthy
-  |> Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts')
+  (raw_dt_names, raw_dts)
 end 
 *}
 
@@ -171,10 +168,14 @@
 ML {* 
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 let
+  val conf = Datatype.default_config
   val dts_names = map (fn (_, s, _, _) => Binding.name_of s) dts
+
+  val (raw_dt_names, raw_dts) = raw_dts_decl dts_names dts lthy
+
 in
   lthy
-  |> raw_dts_decl dts_names dts
+  |> Local_Theory.theory_result (Datatype.add_datatype conf raw_dt_names raw_dts)
   ||>> raw_bn_fun_decl dts_names dts bn_funs bn_eqs
 end
 *}
@@ -242,6 +243,7 @@
 *}
 
 ML {*
+(* associates every SOME with the index in the list *)
 fun mk_env xs =
   let
     fun mapp (_: int) [] = []
@@ -256,14 +258,16 @@
 fun env_lookup xs x =
   case AList.lookup (op =) xs x of
     SOME x => x
-  | NONE => error ("cannot find " ^ x ^ " in the binding specification.")  
+  | NONE => error ("cannot find " ^ x ^ " in the binding specification.");
 *}
 
+
+
 ML {*
 fun prepare_binds dt_strs lthy = 
 let
-  fun extract_cnstrs dt_strs =
-    map ((map (fn (_, antys, _, bns) => (antys, bns))) o forth) dt_strs
+  fun extract_annos_binds dt_strs =
+    map ((map (fn (_, antys, _, bns) => (map fst antys, bns))) o forth) dt_strs
 
   fun prep_bn env bn_str =
     case (Syntax.read_term lthy bn_str) of
@@ -271,20 +275,23 @@
      | Const (a, T) $ Free (x, _) => (env_lookup env x, SOME (Const (a, T)))
      | _ => error (bn_str ^ " not allowed as binding specification.");  
  
-  fun prep_typ env (opt_name, _) = 
+  fun prep_typ env opt_name = 
     case opt_name of
       NONE => []
     | SOME x => find_all (op=) env x;
         
-  fun prep_binds (anno_tys, bind_strs) = 
+  (* 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 (map fst anno_tys)
+    val env = mk_env annos (* for ever label the index *)
     val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs  
   in
-    map (prep_typ binds) anno_tys
+    map (prep_typ binds) annos
   end
+
 in
-  map (map prep_binds) (extract_cnstrs dt_strs)
+  map (map prep_binds) (extract_annos_binds dt_strs)
 end
 *}