--- a/Nominal/Ex/SingleLet.thy	Fri May 21 05:58:23 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Fri May 21 11:40:18 2010 +0100
@@ -19,7 +19,7 @@
 where
   "bn (As x t) = {atom x}"
 
-thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars]
+thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_raw.simps[no_vars]
 
 ML {* Inductive.the_inductive *}
 thm trm_assg.fv

--- a/Nominal/NewParser.thy	Fri May 21 05:58:23 2010 +0100
+++ b/Nominal/NewParser.thy	Fri May 21 11:40:18 2010 +0100
@@ -251,7 +251,7 @@
   
   val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
   val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs 
-  val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds 
+  val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_env binds 
   val raw_bn_descr = prep_bn_descr lthy dt_full_names' raw_dts (map snd raw_bn_eqs)
 
   val (raw_dt_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy
@@ -261,7 +261,7 @@
   fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l);
   val raw_bn_descr_exp = map (export_fun (Morphism.term morphism_2_0)) raw_bn_descr;
 in
-  (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_funs2, raw_bn_eqs2, raw_bn_descr_exp, raw_bn_descr, lthy2)
+  (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_funs2, raw_bn_eqs2, raw_bn_descr_exp, raw_bn_descr, lthy1)
 end
 *}
 
@@ -312,7 +312,7 @@
 
   val _ = tracing ("raw_bn_descr " ^ @{make_string} raw_bn_descr)
   val _ = tracing ("raw_bn_descr2 " ^ @{make_string} raw_bn_descr2)
-  val _ = tracing ("bclauses " ^ @{make_string} bclauses)
+  val _ = tracing ("raw_bclauses " ^ @{make_string} raw_bclauses)
   val _ = tracing ("raw_bn_fund " ^ @{make_string} raw_bn_funs)
   val _ = tracing ("raw_bn_eqs " ^ @{make_string} raw_bn_eqs)
   val _ = tracing ("raw_bn_fund2 " ^ @{make_string} raw_bn_funs2)
@@ -349,7 +349,7 @@
 
   val (fv, fvbn, fv_def, lthy3a) = 
     if get_STEPS lthy2 > 3 
-    then define_raw_fvs (map (fn (x, _, _) => Binding.name_of x) bn_funs) (map snd bn_eqs) descr sorts raw_bn_descr raw_bn_descr2 raw_bclauses lthy3
+    then define_raw_fvs (map (fn (x, _, _) => Binding.name_of x) raw_bn_funs2) (map snd raw_bn_eqs2) descr sorts raw_bn_descr2 raw_bn_descr2 raw_bclauses lthy3
     else raise TEST lthy3
   
 
@@ -575,7 +575,7 @@
   fun prep_binder env bn_str =
     case (Syntax.read_term lthy bn_str) of
       Free (x, _) => (NONE, index_lookup env x)
-    | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x)
+    | Const (a, T) $ Free (x, _) => (SOME (Free (Long_Name.base_name a, T)), index_lookup env x)
     | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.")
  
   fun prep_body env bn_str = index_lookup env bn_str

--- a/Nominal/nominal_dt_rawfuns.ML	Fri May 21 05:58:23 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Fri May 21 11:40:18 2010 +0100
@@ -123,6 +123,17 @@
     NONE => mk_supp arg
   | SOME fv => fv $ arg
 end  
+handle Option  => error "fv_map lookup "
+
+fun mk_fv_binder lthy fv_bn_map args (bn_option, i) = 
+let
+  val arg = nth args i
+in
+  case bn_option of
+    NONE => (setify lthy arg, @{term "{}::atom set"})
+  | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg)
+end  
+handle Option  => error "fv_bn_map lookup "
 
 fun mk_fv_bn_body fv_map fv_bn_map bn_args args i = 
 let
@@ -136,15 +147,7 @@
   | SOME (NONE) => @{term "{}::atom set"}
   | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg
 end  
-
-fun mk_fv_binder lthy fv_bn_map args (bn_option, i) = 
-let
-  val arg = nth args i
-in
-  case bn_option of
-    NONE => (setify lthy arg, @{term "{}::atom set"})
-  | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg)
-end  
+handle Option  => error "fv_map/fv_bn_map lookup "
 
 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
 let
@@ -154,16 +157,13 @@
   fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
 end
 
+(* in case of fv_bn we have to treat the case special, where an
+   "empty" binding clause is given *)
 fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =
   case bclause of
     BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies)
-  | BC (_, binders, bodies) => 
-      let
-        val t1 = map (mk_fv_body fv_map args) bodies
-        val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders)
-      in 
-        fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
-      end
+  | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause
+
 
 fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = 
 let
@@ -223,14 +223,15 @@
 
   val constrs_info = all_dtyp_constrs_types dt_descr sorts
 
-  val fv_eqs2 = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map2)) constrs_info bclausesss 
+  val fv_eqs2 = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map3)) constrs_info bclausesss 
   val fv_bn_eqs2 = map (mk_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2
   
-  val _ = tracing ("functions to be defined\n " ^ @{make_string} (fv_names @ fv_bn_names2))
-  val _ = tracing ("equations\n " ^ cat_lines (map (Syntax.string_of_term lthy) (flat fv_eqs2 @ flat fv_bn_eqs2)))
+  val _ = tracing ("functions to be defined\n " ^ @{make_string} (t1 @ fv_names @ fv_bn_names2))
+  val _ = tracing ("equations\n " ^ 
+    cat_lines (map (Syntax.string_of_term lthy) (t2 @ flat fv_eqs2 @ flat fv_bn_eqs2)))
 
-  val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names2)
-  val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs2 @ flat fv_bn_eqs2)
+  val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (t1 @ fv_names @ fv_bn_names2)
+  val all_fv_eqs = map (pair Attrib.empty_binding) (t2 @ flat fv_eqs2 @ flat fv_bn_eqs2)
 
   fun pat_completeness_auto lthy =
     Pat_Completeness.pat_completeness_tac lthy 1