--- a/Nominal/Ex/SingleLet.thy	Sat May 22 13:51:47 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Sun May 23 02:15:24 2010 +0100
@@ -5,7 +5,7 @@
 atom_decl name
 
 ML {* print_depth 50 *}
-declare [[STEPS = 4]]
+declare [[STEPS = 5]]
 
 
 nominal_datatype trm =
@@ -21,6 +21,8 @@
   "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] bn_raw.simps[no_vars]
+thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
+
 
 ML {* Inductive.the_inductive *}
 thm trm_assg.fv

--- a/Nominal/NewAlpha.thy	Sat May 22 13:51:47 2010 +0100
+++ b/Nominal/NewAlpha.thy	Sun May 23 02:15:24 2010 +0100
@@ -127,7 +127,7 @@
 let
   fun mk_alphabn_free (bn, ith, _) =
     let
-      val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Free bn)));
+      val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));
       val ty = nth_dtyp dt_descr sorts ith;
       val alphabn_type = ty --> ty --> @{typ bool};
       val alphabn_free = Free(alphabn_name, alphabn_type);
@@ -190,10 +190,8 @@
 *}
 
 ML {*
-fun define_raw_alpha (dt_info : Datatype_Aux.info) bn_funs bclausesss fv_frees lthy =
+fun define_raw_alpha dt_descr sorts bn_funs bclausesss fv_frees lthy =
 let
-  val {descr as dt_descr, sorts, ...} = dt_info;
-
   val alpha_names = prefix_dt_names dt_descr sorts "alpha_";
   val alpha_types = map (fn (i, _) =>
     nth_dtyp dt_descr sorts i --> nth_dtyp dt_descr sorts i --> @{typ bool}) dt_descr;
@@ -230,8 +228,9 @@
   val alpha_intros = Morphism.fact morphism alpha_intros_loc
   val alpha_cases = Morphism.fact morphism alpha_cases_loc
 in
-  (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy')
+  (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy')
 end
+handle UnequalLengths => error "Main"
 *}
 
 end

--- a/Nominal/NewParser.thy	Sat May 22 13:51:47 2010 +0100
+++ b/Nominal/NewParser.thy	Sun May 23 02:15:24 2010 +0100
@@ -190,7 +190,7 @@
 *}
 
 ML {*
-fun prep_bn_descr lthy dt_names dts eqs = 
+fun prep_bn_info lthy dt_names dts eqs = 
 let
   fun aux eq = 
   let
@@ -257,15 +257,14 @@
   val raw_dt_names' =  map (Long_Name.qualify thy_name) raw_dt_names
   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_bn_descr = prep_bn_descr lthy dt_full_names' raw_dts (map snd raw_bn_eqs)*)
 
   val (raw_dt_full_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy
-  val (raw_bn_funs2, raw_bn_eqs2, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1
+  val (raw_bn_funs', raw_bn_eqs', lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1
 
-  val raw_bn_descr = 
-    prep_bn_descr lthy dt_full_names' raw_dts (map prop_of raw_bn_eqs2)
+  val raw_bn_info = 
+    prep_bn_info lthy dt_full_names' raw_dts (map prop_of raw_bn_eqs')
 in
-  (raw_dt_full_names, raw_bclauses, raw_bn_funs2, raw_bn_eqs2, raw_bn_descr, lthy2)
+  (raw_dt_full_names, raw_bclauses, raw_bn_funs', raw_bn_eqs', raw_bn_info, lthy2)
 end
 *}
 
@@ -310,8 +309,9 @@
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
   (* definition of the raw datatypes *)
-  val (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_descr, lthy1) =
-    if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
+  val (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_info, lthy1) =
+    if get_STEPS lthy > 1 
+    then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names)
@@ -343,42 +343,46 @@
   (* definition of raw fv_functions *)
   val lthy3 = Theory_Target.init NONE thy;
 
-  val (fv, fvbn, fv_def, lthy3a) = 
+  val (fv, fv_bn, fv_def, lthy3a) = 
     if get_STEPS lthy2 > 3 
-    then define_raw_fvs descr sorts raw_bn_funs raw_bn_descr raw_bclauses lthy3
+    then define_raw_fvs descr sorts raw_bn_info raw_bclauses lthy3
     else raise TEST lthy3
   
 
   (* definition of raw alphas *)
-  val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
+  val (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) =
     if get_STEPS lthy > 4 
-    then define_raw_alpha dtinfo raw_bn_descr raw_bclauses fv lthy3a
+    then define_raw_alpha descr sorts raw_bn_info 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;
-  val bn_tys = map (domain_type o fastype_of) [] (*raw_bn_funs;*)
+  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;
+  val bns = raw_bn_funs ~~ bn_nos;
   val rel_dists = flat (map (distinct_rel lthy4 alpha_cases)
     (rel_distinct ~~ alpha_ts_nobn));
   val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
   
   (* definition of raw_alpha_eq_iff  lemmas *)
-  val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4
+  val alpha_eq_iff = 
+    if get_STEPS lthy > 5
+    then build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4
+    else raise TEST lthy4
+
   val alpha_eq_iff_simp = map remove_loop alpha_eq_iff;
   
   (* 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
-  val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fvbn) lthy5
+  val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fv_bn) lthy5
   val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6;
 
   (* proving alpha equivalence *)
   val _ = warning "Proving equivalence";
-  val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
+  val fv_alpha_all = combine_fv_alpha_bns (fv, fv_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
   val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a;
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts
@@ -407,7 +411,7 @@
   val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
   val (fv_rsp_pre, lthy10) = fold_map
     (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;
+    (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fv_bn) lthy9;
   val fv_rsp = flat (map snd fv_rsp_pre);
   val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
@@ -421,8 +425,8 @@
       in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
     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_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fv_bn)
+  val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fv_bn)) lthy12;
   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;

--- a/Nominal/nominal_dt_rawfuns.ML	Sat May 22 13:51:47 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Sun May 23 02:15:24 2010 +0100
@@ -8,27 +8,26 @@
 
 signature NOMINAL_DT_RAWFUNS =
 sig
-  (* binding modes and binding clauses *)
+  (* info of binding functions *)
+  type bn_info = (term * int * (int * term option) list list) list
 
+  (* binding modes and binding clauses *)
   datatype bmode = Lst | Res | Set
-
   datatype bclause = BC of bmode * (term option * int) list * int list
 
   val setify: Proof.context -> term -> term
   val listify: Proof.context -> term -> term
 
-  val define_raw_fvs: 
-     Datatype_Aux.descr ->
-     (string * sort) 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
+  val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
+    bclause list list list -> Proof.context -> term list * term list * thm list * local_theory
 end
 
 
 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
 struct
 
+type bn_info = (term * int * (int * term option) list list) list
+
 datatype bmode = Lst | Res | Set
 datatype bclause = BC of bmode * (term option * int) list * int list
 
@@ -76,8 +75,8 @@
   Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t
 end
 
-(* functions that coerces concrete atoms, sets and fsets into sets
-   of general atoms *)
+(* functions that coerces singletons, sets and fsets of concrete atoms
+   into sets of general atoms *)
 fun setify ctxt t =
 let
   val ty = fastype_of t;
@@ -91,8 +90,8 @@
   else raise TERM ("setify", [t])
 end
 
-(* functions that coerces concrete atoms and lists into lists of 
-   general atoms  *)
+(* functions that coerces singletons and lists of concrete atoms
+   into lists of general atoms  *)
 fun listify ctxt t =
 let
   val ty = fastype_of t;
@@ -111,42 +110,29 @@
   else t
 
 
-(* functions that construct the equations for fv and fv_bn *)
-
-fun mk_fv_body fv_map args i = 
-let
-  val arg = nth args i
-  val ty = fastype_of arg
-in
-  case (AList.lookup (op=) fv_map ty) of
-    NONE => mk_supp arg
-  | SOME fv => fv $ 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  
-
-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
-in
-  case AList.lookup (op=) bn_args i of
-    NONE => (case (AList.lookup (op=) fv_map ty) of
-              NONE => mk_supp arg
-            | SOME fv => fv $ arg)
-  | SOME (NONE) => @{term "{}::atom set"}
-  | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg
-end  
+(** functions that construct the equations for fv and fv_bn **)
 
 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
 let
+  fun mk_fv_body fv_map args i = 
+  let
+    val arg = nth args i
+    val ty = fastype_of arg
+  in
+    case AList.lookup (op=) fv_map ty of
+      NONE => mk_supp arg
+    | SOME fv => fv $ 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  
+
   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 
@@ -156,10 +142,24 @@
 (* 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 =
+let
+  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
+  in
+    case AList.lookup (op=) bn_args i of
+      NONE => (case (AList.lookup (op=) fv_map ty) of
+                 NONE => mk_supp arg
+              | SOME fv => fv $ arg)
+    | SOME (NONE) => @{term "{}::atom set"}
+    | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg
+  end  
+in
   case bclause of
     BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies)
   | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause
-
+end
 
 fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = 
 let
@@ -193,28 +193,29 @@
   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_trms bn_funs2 bclausesss lthy =
+fun define_raw_fvs descr sorts bn_info bclausesss lthy =
 let
-  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_names = prefix_dt_names descr sorts "fv_"
+  val fv_arg_tys = map (fn (i, _) => nth_dtyp descr sorts i) 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 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_map = bn_trms ~~ fv_bn_frees2
+  val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
+  val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
+  val fv_bn_names = map (prefix "fv_") bn_names
+  val fv_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys
+  val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys
+  val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys)
+  val fv_bn_map = bns ~~ fv_bn_frees
 
-  val constrs_info = all_dtyp_constrs_types dt_descr sorts
+  val constrs_info = all_dtyp_constrs_types descr sorts
 
-  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 fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) constrs_info bclausesss 
+  val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_info
   
-  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_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
+  val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
 
   fun pat_completeness_auto lthy =
     Pat_Completeness.pat_completeness_tac lthy 1
@@ -224,7 +225,7 @@
     Function.prove_termination NONE
       (Lexicographic_Order.lexicographic_order_tac true lthy) lthy
 
-  val (_, lthy') = Function.add_function all_fv_names all_fv_eqs
+  val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
     Function_Common.default_config pat_completeness_auto lthy
 
   val (info, lthy'') = prove_termination (Local_Theory.restore lthy')

--- a/Nominal/nominal_dt_rawperm.ML	Sat May 22 13:51:47 2010 +0100
+++ b/Nominal/nominal_dt_rawperm.ML	Sun May 23 02:15:24 2010 +0100
@@ -27,7 +27,6 @@
     - in case the argument is non-recursive it will return
 
          p o arg
-
 *)
 fun perm_arg permute_fn_frees p (arg_dty, arg) =
   if Datatype_Aux.is_rec_type arg_dty