--- a/Nominal/nominal_dt_rawfuns.ML	Fri May 21 11:40:18 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Sat May 22 13:51:47 2010 +0100
@@ -18,10 +18,9 @@
   val listify: Proof.context -> term -> term
 
   val define_raw_fvs: 
-     string list -> term list -> 
      Datatype_Aux.descr ->
      (string * sort) list ->
-     (term * int * (int * term option) list list) list ->
+     term list ->
      (term * int * (int * term option) list list) list ->
      bclause list list list -> Proof.context -> term list * term list * thm list * local_theory
 end
@@ -123,7 +122,6 @@
     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
@@ -133,7 +131,6 @@
     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
@@ -147,7 +144,6 @@
   | SOME (NONE) => @{term "{}::atom set"}
   | SOME (SOME bn) => 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
@@ -197,41 +193,28 @@
   map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
 end
 
-fun define_raw_fvs t1 t2 dt_descr sorts bn_funs bn_funs2 bclausesss lthy =
+fun define_raw_fvs dt_descr sorts bn_trms bn_funs2 bclausesss lthy =
 let
-  val _ = tracing ("bn-functions to be defined\n " ^ commas t1)
-  val _ = tracing ("bn-equations\n " ^ cat_lines (map (Syntax.string_of_term lthy) t2))
-
   val fv_names = prefix_dt_names dt_descr sorts "fv_"
   val fv_arg_tys = map (fn (i, _) => nth_dtyp dt_descr sorts i) dt_descr;
   val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;
   val fv_frees = map Free (fv_names ~~ fv_tys);
   val fv_map = fv_arg_tys ~~ fv_frees
 
-  val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs)
-  val (bns2, bn_tys2) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs2)
-  val bn_args2 = map (fn (_, _, arg) => arg) bn_funs2
-  val fv_bn_names2 = map (fn bn => "fv_" ^ (fst (dest_Free bn))) bns2
+  val bn_tys2 = map (fn (_, i, _) => i) bn_funs2
+  val fv_bn_names2 = map (fn bn => "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)))) bn_trms
   val fv_bn_arg_tys2 = map (fn i => nth_dtyp dt_descr sorts i) bn_tys2
   val fv_bn_tys2 = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys2
   val fv_bn_frees2 = map Free (fv_bn_names2 ~~ fv_bn_tys2)
-  val fv_bn_map2 = bns ~~ fv_bn_frees2
-  val fv_bn_map3 = bns2 ~~ fv_bn_frees2
- 
-  val _ = tracing ("fn_bn_map2 " ^ @{make_string} fv_bn_map2)
-  val _ = tracing ("fn_bn_map3 " ^ @{make_string} fv_bn_map3)
+  val fv_bn_map = bn_trms ~~ fv_bn_frees2
 
   val constrs_info = all_dtyp_constrs_types dt_descr sorts
 
-  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 fv_eqs2 = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) constrs_info bclausesss 
+  val fv_bn_eqs2 = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_funs2
   
-  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)) (t1 @ fv_names @ fv_bn_names2)
-  val all_fv_eqs = map (pair Attrib.empty_binding) (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)
 
   fun pat_completeness_auto lthy =
     Pat_Completeness.pat_completeness_tac lthy 1