--- a/Nominal/Ex/SingleLet.thy	Fri May 21 00:44:39 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Fri May 21 05:58:23 2010 +0100
@@ -5,7 +5,7 @@
 atom_decl name
 
 ML {* print_depth 50 *}
-declare [[STEPS = 19]]
+declare [[STEPS = 4]]
 
 nominal_datatype trm =
   Var "name"

--- a/Nominal/NewParser.thy	Fri May 21 00:44:39 2010 +0100
+++ b/Nominal/NewParser.thy	Fri May 21 05:58:23 2010 +0100
@@ -185,7 +185,7 @@
 *}
 
 ML {*
-fun prep_bn lthy dt_names dts eqs = 
+fun prep_bn_descr lthy dt_names dts eqs = 
 let
   fun aux eq = 
   let
@@ -252,16 +252,16 @@
   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_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs)
+  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
-  val (raw_bn_funs, raw_bn_eqs, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1
+  val (raw_bn_funs2, raw_bn_eqs2, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1
 
   val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
   fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l);
-  val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns;
+  val raw_bn_descr_exp = map (export_fun (Morphism.term morphism_2_0)) raw_bn_descr;
 in
-  (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, raw_bns, 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, lthy2)
 end
 *}
 
@@ -290,70 +290,6 @@
   handle TERM _ => @{thm eqTrueI} OF [t]
 *}
 
-text {* 
-  nominal_datatype2 does the following things in order:
-
-Parser.thy/raw_nominal_decls
-  1) define the raw datatype
-  2) define the raw binding functions 
-
-Perm.thy/define_raw_perms
-  3) define permutations of the raw datatype and show that the raw type is 
-     in the pt typeclass
-      
-Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha
-  4) define fv and fv_bn
-  5) define alpha and alpha_bn
-
-Perm.thy/distinct_rel
-  6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...)             (Proof by cases; simp)
-
-Tacs.thy/build_rel_inj
-  6) prove alpha_eq_iff    (C1 x = C2 y \<leftrightarrow> P x y ...)
-     (left-to-right by intro rule, right-to-left by cases; simp)
-Equivp.thy/prove_eqvt
-  7) prove bn_eqvt (common induction on the raw datatype)
-  8) prove fv_eqvt (common induction on the raw datatype with help of above)
-Rsp.thy/build_alpha_eqvts
-  9) prove alpha_eqvt and alpha_bn_eqvt
-     (common alpha-induction, unfolding alpha_gen, permute of #* and =)
-Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps
- 10) prove that alpha and alpha_bn are equivalence relations
-     (common induction and application of 'compose' lemmas)
-Lift.thy/define_quotient_types
- 11) define quotient types
-Rsp.thy/build_fvbv_rsps
- 12) prove bn respects     (common induction and simp with alpha_gen)
-Rsp.thy/prove_const_rsp
- 13) prove fv respects     (common induction and simp with alpha_gen)
- 14) prove permute respects    (unfolds to alpha_eqvt)
-Rsp.thy/prove_alpha_bn_rsp
- 15) prove alpha_bn respects
-     (alpha_induct then cases then sym and trans of the relations)
-Rsp.thy/prove_alpha_alphabn
- 16) show that alpha implies alpha_bn (by unduction, needed in following step)
-Rsp.thy/prove_const_rsp
- 17) prove respects for all datatype constructors
-     (unfold eq_iff and alpha_gen; introduce zero permutations; simp)
-Perm.thy/quotient_lift_consts_export
- 18) define lifted constructors, fv, bn, alpha_bn, permutations
-Perm.thy/define_lifted_perms
- 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass
-Lift.thy/lift_thm
- 20) lift permutation simplifications
- 21) lift induction
- 22) lift fv
- 23) lift bn
- 24) lift eq_iff
- 25) lift alpha_distincts
- 26) lift fv and bn eqvts
-Equivp.thy/prove_supports
- 27) prove that union of arguments supports constructors
-Equivp.thy/prove_fs
- 28) show that the lifted type is in fs typeclass     (* by q_induct, supports *)
-Equivp.thy/supp_eq
- 29) prove supp = fv
-*}
 
 ML {*
 (* for testing porposes - to exit the procedure early *)
@@ -370,12 +306,17 @@
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
   (* definition of the raw datatypes and raw bn-functions *)
-  val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, raw_bns2, lthy1) =
+  val (raw_dt_names, raw_bclauses, raw_bn_funs2, raw_bn_eqs2, raw_bn_funs, raw_bn_eqs, raw_bn_descr, raw_bn_descr2, lthy1) =
     if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
-  (*val _ = tracing ("exported: " ^ commas (map @{make_string} raw_bns))*)
-  (*val _ = tracing ("plain: " ^ commas (map @{make_string} raw_bns2))*)
+  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_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)
+  val _ = tracing ("raw_bn_eqs2 " ^ cat_lines (map (Syntax.string_of_term lthy o snd) raw_bn_eqs2))
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo
@@ -391,7 +332,7 @@
   val exhaust_thms = map #exhaust dtinfos;
 
   (* definitions of raw permutations *)
-  val ((perms, raw_perm_defs, raw_perm_simps), lthy2) =
+  val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) =
     if get_STEPS lthy1 > 2 
     then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1
     else raise TEST lthy1
@@ -405,22 +346,22 @@
 
   (* definition of raw fv_functions *)
   val lthy3 = Theory_Target.init NONE thy;
-  val raw_bn_funs = map (fn (f, _, _) => f) raw_bns;
 
   val (fv, fvbn, fv_def, lthy3a) = 
     if get_STEPS lthy2 > 3 
-    then define_raw_fvs descr sorts raw_bns raw_bns2 raw_bclauses lthy3
+    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
     else raise TEST lthy3
   
+
   (* definition of raw alphas *)
   val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
     if get_STEPS lthy > 4 
-    then define_raw_alpha dtinfo raw_bns raw_bclauses fv lthy3a
+    then define_raw_alpha dtinfo raw_bn_descr raw_bclauses fv lthy3a
     else raise TEST lthy3a
   
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
   
-  val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
+  val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr;
   val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
   val bns = raw_bn_funs ~~ bn_nos;
@@ -433,8 +374,6 @@
   val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4
   val alpha_eq_iff_simp = map remove_loop alpha_eq_iff;
   
-  (*val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp);*)
-
   (* proving equivariance lemmas *)
   val _ = warning "Proving equivariance";
   val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4
@@ -474,7 +413,7 @@
     (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
     (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9;
   val fv_rsp = flat (map snd fv_rsp_pre);
-  val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms
+  val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
   fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy
     else
@@ -488,7 +427,7 @@
     const_rsp_tac) raw_consts lthy11a
     val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn)
   val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12;
-  val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;
+  val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts;
   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
   val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a;
   val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn
@@ -497,7 +436,7 @@
   val _ = warning "Lifting permutations";
   val thy = Local_Theory.exit_global lthy12c;
   val perm_names = map (fn x => "permute_" ^ x) qty_names
-  val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
+  val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ raw_perm_funs) raw_perm_simps thy;
   val lthy13 = Theory_Target.init NONE thy';
   val q_name = space_implode "_" qty_names;
   fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
@@ -717,108 +656,71 @@
   (main_parser >> nominal_datatype2_cmd)
 *}
 
-(*
-atom_decl name
+
+text {* 
+  nominal_datatype2 does the following things in order:
 
-nominal_datatype lam =
-  Var name
-| App lam lam
-| Lam x::name t::lam  bind_set x in t
-| Let p::pt t::lam bind_set "bn p" in t
-and pt =
-  P1 name
-| P2 pt pt
-binder
- bn::"pt \<Rightarrow> atom set"
-where
-  "bn (P1 x) = {atom x}"
-| "bn (P2 p1 p2) = bn p1 \<union> bn p2"
-
-find_theorems Var_raw
-
-
+Parser.thy/raw_nominal_decls
+  1) define the raw datatype
+  2) define the raw binding functions 
 
-thm lam_pt.bn
-thm lam_pt.fv[simplified lam_pt.supp(1-2)]
-thm lam_pt.eq_iff
-thm lam_pt.induct
-thm lam_pt.perm
-
-nominal_datatype exp =
-  EVar name
-| EUnit
-| EPair q1::exp q2::exp
-| ELetRec l::lrbs e::exp     bind "b_lrbs l" in e l
+Perm.thy/define_raw_perms
+  3) define permutations of the raw datatype and show that the raw type is 
+     in the pt typeclass
+      
+Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha
+  4) define fv and fv_bn
+  5) define alpha and alpha_bn
 
-and fnclause =
-  K x::name p::pat f::exp    bind_res "b_pat p" in f
-
-and fnclauses =
-  S fnclause
-| ORs fnclause fnclauses
-
-and lrb =
-  Clause fnclauses
-
-and lrbs =
-  Single lrb
-| More lrb lrbs
+Perm.thy/distinct_rel
+  6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...)             (Proof by cases; simp)
 
-and pat =
-  PVar name
-| PUnit
-| PPair pat pat
-
-binder
-  b_lrbs      :: "lrbs \<Rightarrow> atom list" and
-  b_pat       :: "pat \<Rightarrow> atom set" and
-  b_fnclauses :: "fnclauses \<Rightarrow> atom list" and
-  b_fnclause  :: "fnclause \<Rightarrow> atom list" and
-  b_lrb       :: "lrb \<Rightarrow> atom list"
-
-where
-  "b_lrbs (Single l) = b_lrb l"
-| "b_lrbs (More l ls) = append (b_lrb l) (b_lrbs ls)"
-| "b_pat (PVar x) = {atom x}"
-| "b_pat (PUnit) = {}"
-| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
-| "b_fnclauses (S fc) = (b_fnclause fc)"
-| "b_fnclauses (ORs fc fcs) = append (b_fnclause fc) (b_fnclauses fcs)"
-| "b_lrb (Clause fcs) = (b_fnclauses fcs)"
-| "b_fnclause (K x pat exp) = [atom x]"
-
-thm exp_fnclause_fnclauses_lrb_lrbs_pat.bn
-thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv
-thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff
-thm exp_fnclause_fnclauses_lrb_lrbs_pat.induct
-thm exp_fnclause_fnclauses_lrb_lrbs_pat.perm
-
-nominal_datatype ty =
-  Vr "name"
-| Fn "ty" "ty"
-and tys =
-  Al xs::"name fset" t::"ty" bind_res xs in t
-
-thm ty_tys.fv[simplified ty_tys.supp]
-thm ty_tys.eq_iff
-
-*)
-
-(* some further tests *)
-
-(*
-nominal_datatype ty2 =
-  Vr2 "name"
-| Fn2 "ty2" "ty2"
-
-nominal_datatype tys2 =
-  All2 xs::"name fset" ty::"ty2" bind_res xs in ty
-
-nominal_datatype lam2 =
-  Var2 "name"
-| App2 "lam2" "lam2 list"
-| Lam2 x::"name" t::"lam2" bind x in t
-*)
+Tacs.thy/build_rel_inj
+  6) prove alpha_eq_iff    (C1 x = C2 y \<leftrightarrow> P x y ...)
+     (left-to-right by intro rule, right-to-left by cases; simp)
+Equivp.thy/prove_eqvt
+  7) prove bn_eqvt (common induction on the raw datatype)
+  8) prove fv_eqvt (common induction on the raw datatype with help of above)
+Rsp.thy/build_alpha_eqvts
+  9) prove alpha_eqvt and alpha_bn_eqvt
+     (common alpha-induction, unfolding alpha_gen, permute of #* and =)
+Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps
+ 10) prove that alpha and alpha_bn are equivalence relations
+     (common induction and application of 'compose' lemmas)
+Lift.thy/define_quotient_types
+ 11) define quotient types
+Rsp.thy/build_fvbv_rsps
+ 12) prove bn respects     (common induction and simp with alpha_gen)
+Rsp.thy/prove_const_rsp
+ 13) prove fv respects     (common induction and simp with alpha_gen)
+ 14) prove permute respects    (unfolds to alpha_eqvt)
+Rsp.thy/prove_alpha_bn_rsp
+ 15) prove alpha_bn respects
+     (alpha_induct then cases then sym and trans of the relations)
+Rsp.thy/prove_alpha_alphabn
+ 16) show that alpha implies alpha_bn (by unduction, needed in following step)
+Rsp.thy/prove_const_rsp
+ 17) prove respects for all datatype constructors
+     (unfold eq_iff and alpha_gen; introduce zero permutations; simp)
+Perm.thy/quotient_lift_consts_export
+ 18) define lifted constructors, fv, bn, alpha_bn, permutations
+Perm.thy/define_lifted_perms
+ 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass
+Lift.thy/lift_thm
+ 20) lift permutation simplifications
+ 21) lift induction
+ 22) lift fv
+ 23) lift bn
+ 24) lift eq_iff
+ 25) lift alpha_distincts
+ 26) lift fv and bn eqvts
+Equivp.thy/prove_supports
+ 27) prove that union of arguments supports constructors
+Equivp.thy/prove_fs
+ 28) show that the lifted type is in fs typeclass     (* by q_induct, supports *)
+Equivp.thy/supp_eq
+ 29) prove supp = fv
+*}
 
 
 

--- a/Nominal/nominal_dt_rawfuns.ML	Fri May 21 00:44:39 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Fri May 21 05:58:23 2010 +0100
@@ -17,9 +17,13 @@
   val setify: Proof.context -> term -> term
   val listify: Proof.context -> term -> term
 
-  val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list ->
-    (term * 'a * 'b) list -> (term * int * (int * term option) list list) list ->
-      bclause list list list -> Proof.context -> term list * term list * thm list * local_theory
+  val define_raw_fvs: 
+     string list -> term list -> 
+     Datatype_Aux.descr ->
+     (string * sort) list ->
+     (term * int * (int * term option) list list) list ->
+     (term * int * (int * term option) list list) list ->
+     bclause list list list -> Proof.context -> term list * term list * thm list * local_theory
 end
 
 
@@ -29,7 +33,7 @@
 datatype bmode = Lst | Res | Set
 datatype bclause = BC of bmode * (term option * int) list * int list
 
-(* atom types *)
+(* testing for concrete atom types *)
 fun is_atom ctxt ty =
   Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
 
@@ -43,15 +47,16 @@
   | is_atom_list _ _ = false
 
 
-(* functions for producing sets, fsets and lists *)
+(* functions for producing sets, fsets and lists of general atom type
+   out from concrete atom types *)
 fun mk_atom_set t =
 let
   val ty = fastype_of t;
   val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};
   val img_ty = atom_ty --> ty --> @{typ "atom set"};
 in
-  (Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t)
-end;
+  Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
+end
 
 fun mk_atom_fset t =
 let
@@ -61,20 +66,19 @@
   val fset_to_set = @{term "fset_to_set :: atom fset => atom set"}
 in
   fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
-end;
+end
 
-(*
 fun mk_atom_list t =
 let
   val ty = fastype_of t;
   val atom_ty = dest_listT ty --> @{typ atom};
   val map_ty = atom_ty --> ty --> @{typ "atom list"};
 in
-  (Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t)
-end;
-*)
+  Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t
+end
 
-(* functions that coerces atoms, sets and fsets into atom sets ? *)
+(* functions that coerces concrete atoms, sets and fsets into sets
+   of general atoms *)
 fun setify ctxt t =
 let
   val ty = fastype_of t;
@@ -88,7 +92,8 @@
   else raise TERM ("setify", [t])
 end
 
-(* functions that coerces atoms and lists into atom lists ? *)
+(* functions that coerces concrete atoms and lists into lists of 
+   general atoms  *)
 fun listify ctxt t =
 let
   val ty = fastype_of t;
@@ -109,7 +114,7 @@
 
 (* functions that construct the equations for fv and fv_bn *)
 
-fun make_fv_body fv_map args i = 
+fun mk_fv_body fv_map args i = 
 let
   val arg = nth args i
   val ty = fastype_of arg
@@ -119,37 +124,7 @@
   | SOME fv => fv $ arg
 end  
 
-fun make_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  
-
-fun make_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
-let
-  val t1 = map (make_fv_body fv_map args) bodies
-  val (t2, t3) = split_list (map (make_fv_binder lthy fv_bn_map args) binders)
-in 
-  fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
-end
-
-fun make_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = 
-let
-  val arg_names = Datatype_Prop.make_tnames arg_tys
-  val args = map Free (arg_names ~~ arg_tys)
-  val fv = the (AList.lookup (op=) fv_map ty)
-  val lhs = fv $ list_comb (constr, args)
-  val rhs_trms = map (make_fv_rhs lthy fv_map fv_bn_map args) bclauses
-  val rhs = fold_union rhs_trms
-in
-  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
-end
-
-
-fun make_fv_bn_body fv_map fv_bn_map bn_args args i = 
+fun mk_fv_bn_body fv_map fv_bn_map bn_args args i = 
 let
   val arg = nth args i
   val ty = fastype_of arg
@@ -162,39 +137,70 @@
   | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg
 end  
 
-fun make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =
+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  
+
+fun mk_fv_rhs lthy fv_map fv_bn_map args (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
+
+fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =
   case bclause of
-    BC (_, [], bodies) => fold_union (map (make_fv_bn_body fv_map fv_bn_map bn_args args) bodies)
+    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 (make_fv_body fv_map args) bodies
-        val (t2, t3) = split_list (map (make_fv_binder lthy fv_bn_map args) binders)
+        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
 
-fun make_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys)) bclauses =
+fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = 
+let
+  val arg_names = Datatype_Prop.make_tnames arg_tys
+  val args = map Free (arg_names ~~ arg_tys)
+  val fv = the (AList.lookup (op=) fv_map ty)
+  val lhs = fv $ list_comb (constr, args)
+  val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses
+  val rhs = fold_union rhs_trms
+in
+  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+end
+
+fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys)) bclauses =
 let
   val arg_names = Datatype_Prop.make_tnames arg_tys
   val args = map Free (arg_names ~~ arg_tys)
   val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm)
   val lhs = fv_bn $ list_comb (constr, args)
-  val rhs_trms = map (make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses
+  val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses
   val rhs = fold_union rhs_trms
 in
   HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
 end
 
-fun make_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = 
+fun mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = 
 let
   val nth_constrs_info = nth constrs_info bn_n
   val nth_bclausess = nth bclausesss bn_n
 in
-  map2 (make_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
+  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 dt_descr sorts bn_funs bn_funs2 bclausesss lthy =
+fun define_raw_fvs t1 t2 dt_descr sorts bn_funs 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;
@@ -212,11 +218,17 @@
   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 constrs_info = all_dtyp_constrs_types dt_descr sorts
 
-  val fv_eqs2 = map2 (map2 (make_fv_eq lthy fv_map fv_bn_map2)) constrs_info bclausesss 
-  val fv_bn_eqs2 = map (make_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_map2)) 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 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)
 

--- a/Nominal/nominal_dt_rawperm.ML	Fri May 21 00:44:39 2010 +0100
+++ b/Nominal/nominal_dt_rawperm.ML	Fri May 21 05:58:23 2010 +0100
@@ -103,7 +103,7 @@
 (* user_dt_nos refers to the number of "un-unfolded" datatypes
    given by the user
 *)
-fun define_raw_perms (dt_descr:Datatype.descr) sorts induct_thm user_dt_nos thy =
+fun define_raw_perms dt_descr sorts induct_thm user_dt_nos thy =
 let
   val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;
   val user_full_tnames = List.take (all_full_tnames, user_dt_nos);