--- a/Nominal/Parser.thy	Sat Mar 27 09:56:35 2010 +0100
+++ b/Nominal/Parser.thy	Sat Mar 27 12:01:28 2010 +0100
@@ -157,22 +157,18 @@
 *}
 
 ML {*
-fun strip_union t =
+fun strip_bn_fun 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 sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
+  | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
+  | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y =>
+      (i, NONE) :: strip_bn_fun y
+  | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y =>
+      (i, NONE) :: strip_bn_fun 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"
+  | Const (@{const_name Nil}, _) => []
+  | (f as Free _) $ Bound i => [(i, SOME f)]
+  | _ => error ("Unsupported binding function: " ^ (PolyML.makestring t))
 *}
 
 ML {*
@@ -189,7 +185,7 @@
     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 rhs_elements = map bn_or_atom (strip_union rhs)
+    val rhs_elements = strip_bn_fun rhs
     val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements
   in
     (dt_index, (bn_fun, (cnstr_head, included)))

--- a/TODO	Sat Mar 27 09:56:35 2010 +0100
+++ b/TODO	Sat Mar 27 12:01:28 2010 +0100
@@ -42,3 +42,7 @@
 
 - fv_rsp uses 'blast' to show goals of the type:
   a u b = c u d   ==>  a u x u b = c u x u d
+
+When cleaning:
+
+- remove all 'PolyML.makestring'.
\ No newline at end of file