diff -r 9911824a5396 -r ed89a26b7074 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Sat Mar 27 06:51:13 2010 +0100
+++ b/Nominal/Parser.thy	Sat Mar 27 08:11:11 2010 +0100
@@ -141,10 +141,14 @@
 end 
 *}
 
+ML {*
+fun apfst3 f (a, b, c) = (f a, b, c)
+*}
+
 ML {* 
 fun rawify_binds dts_env cnstrs_env bn_fun_env binds =
-  map (map (map (map (fn (opt_trm, i, j) => 
-    (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j))))) binds
+  map (map (map (map (fn (opt_trm, i, j, aty) => 
+    (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j, aty))))) binds
 *}
 
 ML {*
@@ -152,8 +156,6 @@
   | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y
 *}
 
-ML {* @{term "{x, y}"} *}
-ML range_type
 ML {*
 fun strip_union t =
   case t of
@@ -291,9 +293,6 @@
 ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
 ML {* val cheat_const_rsp = Unsynchronized.ref false *}
 
-ML {* fun map_option _ NONE = NONE
-        | map_option f (SOME x) = SOME (f x) *}
-
 (* nominal_datatype2 does the following things in order:
   1) define the raw datatype
   2) define the raw binding functions
@@ -340,7 +339,7 @@
   val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) =
     raw_nominal_decls dts bn_funs bn_eqs binds lthy
   val morphism_2_1 = ProofContext.export_morphism lthy2 lthy
-  fun export_fun f (t, l) = (f t, map (map (apsnd (map_option f))) l);
+  fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
   val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_1)))) raw_bns;
   val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
   val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc
@@ -572,6 +571,7 @@
 
 ML {*
 val recursive = Unsynchronized.ref false
+val alpha_type = Unsynchronized.ref AlphaGen
 *}
 
 ML {*
@@ -602,7 +602,8 @@
   end
 
 in
-  map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))
+  map (map (map (map (fn (a, b, c) => (a, b, c, !alpha_type)))))
+  (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs)))
 end
 *}