--- a/Nominal/Parser.thy	Tue Mar 23 11:43:09 2010 +0100
+++ b/Nominal/Parser.thy	Tue Mar 23 16:28:29 2010 +0100
@@ -152,6 +152,27 @@
   | 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
+    Const (@{const_name sup}, _) $ l $ r => strip_union l @ strip_union r
+  | (h as (Const (@{const_name insert}, T))) $ x $ y =>
+     (h $ x $ Const (@{const_name bot}, range_type (range_type T))) :: strip_union y
+  | Const (@{const_name bot}, _) => []
+  | _ => [t]
+*}
+
+ML {*
+fun bn_or_atom t =
+  case t of
+    Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ 
+      Const (@{const_name bot}, _) => (i, NONE)
+  | f $ Bound i => (i, SOME f)
+  | _ => error "Unsupported binding function"
+*}
+
 ML {*
 fun prep_bn dt_names dts eqs = 
 let
@@ -166,11 +187,11 @@
     val (ty_name, _) = dest_Type (domain_type ty)
     val dt_index = find_index (fn x => x = ty_name) dt_names
     val (cnstr_head, cnstr_args) = strip_comb cnstr
-    val included = map (fn i => length (cnstr_args) - i - 1) (loose_bnos rhs)
+    val rhs_elements = map bn_or_atom (strip_union rhs)
+    val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements
   in
     (dt_index, (bn_fun, (cnstr_head, included)))
   end 
- 
   fun order dts i ts = 
   let
     val dt = nth dts i
@@ -274,6 +295,8 @@
 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
 
+ML {* fun map_option _ NONE = NONE
+        | map_option f (SOME x) = SOME (f x) *}
 
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
@@ -284,7 +307,8 @@
   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
-  val raw_bns_exp = map (apsnd (map (apfst (Morphism.term morphism_2_1)))) raw_bns;
+  fun export_fun f (t, l) = (f t, map (map (apsnd (map_option 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
   val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc