--- a/Nominal/Ex/ExPS8.thy	Thu Aug 26 02:08:00 2010 +0800
+++ b/Nominal/Ex/ExPS8.thy	Fri Aug 27 02:03:52 2010 +0800
@@ -6,6 +6,8 @@
 
 atom_decl name
 
+declare [[STEPS = 15]]
+
 nominal_datatype exp =
   EVar name
 | EUnit

--- a/Nominal/Ex/Let.thy	Thu Aug 26 02:08:00 2010 +0800
+++ b/Nominal/Ex/Let.thy	Fri Aug 27 02:03:52 2010 +0800
@@ -20,6 +20,7 @@
   "bn Lnil = []"
 | "bn (Lcons x t l) = (atom x) # (bn l)"
 
+text {* *}
 
 (*
 

--- a/Nominal/Ex/LetRec.thy	Thu Aug 26 02:08:00 2010 +0800
+++ b/Nominal/Ex/LetRec.thy	Fri Aug 27 02:03:52 2010 +0800
@@ -2,22 +2,20 @@
 imports "../NewParser"
 begin
 
-declare [[STEPS = 14]]
-
 atom_decl name
 
 nominal_datatype let_rec:
- lam =
+ trm =
   Var "name"
-| App "lam" "lam"
-| Lam x::"name" t::"lam"     bind (set) x in t
-| Let_Rec bp::"bp" t::"lam"  bind (set) "bi bp" in bp t
+| App "trm" "trm"
+| Lam x::"name" t::"trm"     bind (set) x in t
+| Let_Rec bp::"bp" t::"trm"  bind (set) "bn bp" in bp t
 and bp =
-  Bp "name" "lam"
+  Bp "name" "trm"
 binder
-  bi::"bp \<Rightarrow> atom set"
+  bn::"bp \<Rightarrow> atom set"
 where
-  "bi (Bp x t) = {atom x}"
+  "bn (Bp x t) = {atom x}"
 
 thm let_rec.distinct
 thm let_rec.induct

--- a/Nominal/Ex/LetRec2.thy	Thu Aug 26 02:08:00 2010 +0800
+++ b/Nominal/Ex/LetRec2.thy	Fri Aug 27 02:03:52 2010 +0800
@@ -4,6 +4,7 @@
 
 atom_decl name
 
+
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
@@ -19,14 +20,12 @@
 | "bn (Lcons x t l) = (atom x) # (bn l)"
 
 
-thm trm_lts.fv
+thm trm_lts.fv_defs
 thm trm_lts.eq_iff
-thm trm_lts.bn
-thm trm_lts.perm
+thm trm_lts.bn_defs
+thm trm_lts.perm_simps
 thm trm_lts.induct
 thm trm_lts.distinct
-thm trm_lts.supp
-thm trm_lts.fv[simplified trm_lts.supp]
 
 
 (* why is this not in HOL simpset? *)
@@ -75,7 +74,7 @@
   apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
   apply (simp add: atom_eqvt fresh_star_def)
   done
-
+*)
 end
 
 

--- a/Nominal/NewParser.thy	Thu Aug 26 02:08:00 2010 +0800
+++ b/Nominal/NewParser.thy	Fri Aug 27 02:03:52 2010 +0800
@@ -330,7 +330,7 @@
     mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys
 
   (* definition of alpha_eq_iff  lemmas *)
-  (* they have a funny shape for the simplifier *)
+  (* they have a funny shape for the simplifier ---- CHECK WHETHER NEEDED*)
   val _ = warning "Eq-iff theorems";
   val (alpha_eq_iff_simps, alpha_eq_iff) = 
     if get_STEPS lthy > 5
@@ -402,24 +402,44 @@
     else raise TEST lthy6
   
   (* respectfulness proofs *)
-  val raw_funs_rsp_aux = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs 
-    raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6
-  val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux
+  val raw_funs_rsp_aux = 
+    if get_STEPS lthy > 15
+    then raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs 
+      raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6
+    else raise TEST lthy6 
+  
+  val raw_funs_rsp = 
+    if get_STEPS lthy > 16
+    then map mk_funs_rsp raw_funs_rsp_aux
+    else raise TEST lthy6 
 
-  val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct 
-    (raw_size_thms @ raw_size_eqvt) lthy6
-    |> map mk_funs_rsp
+  val raw_size_rsp = 
+    if get_STEPS lthy > 17
+    then
+      raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct 
+      (raw_size_thms @ raw_size_eqvt) lthy6
+      |> map mk_funs_rsp
+    else raise TEST lthy6 
 
-  val raw_constrs_rsp = raw_constrs_rsp raw_constrs alpha_trms alpha_intros
-    (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 
+  val raw_constrs_rsp = 
+    if get_STEPS lthy > 18
+    then raw_constrs_rsp raw_constrs alpha_trms alpha_intros
+      (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 
+    else raise TEST lthy6 
 
-  val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
+  val alpha_permute_rsp = 
+    if get_STEPS lthy > 19
+    then map mk_alpha_permute_rsp alpha_eqvt
+    else raise TEST lthy6 
 
-  val alpha_bn_rsp = raw_alpha_bn_rsp alpha_bn_equivp_thms alpha_bn_imp_thms
+  val alpha_bn_rsp = 
+    if get_STEPS lthy > 20
+    then raw_alpha_bn_rsp alpha_bn_equivp_thms alpha_bn_imp_thms
+    else raise TEST lthy6 
 
   (* noting the quot_respects lemmas *)
   val (_, lthy6a) = 
-    if get_STEPS lthy > 15
+    if get_STEPS lthy > 21
     then Local_Theory.note ((Binding.empty, [rsp_attrib]),
       raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6
     else raise TEST lthy6
@@ -429,7 +449,7 @@
   val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
      
   val (qty_infos, lthy7) = 
-    if get_STEPS lthy > 16
+    if get_STEPS lthy > 22
     then define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a
     else raise TEST lthy6a
 
@@ -462,7 +482,7 @@
     map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms
 
   val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = 
-    if get_STEPS lthy > 17
+    if get_STEPS lthy > 23
     then 
       lthy7
       |> define_qconsts qtys qconstrs_descr 
@@ -474,12 +494,12 @@
 
   (* definition of the quotient permfunctions and pt-class *)
   val lthy9 = 
-    if get_STEPS lthy > 18
+    if get_STEPS lthy > 24
     then define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8 
     else raise TEST lthy8
   
   val lthy9a = 
-    if get_STEPS lthy > 19
+    if get_STEPS lthy > 25
     then define_qsizes qtys qty_full_names tvs qsize_descr lthy9
     else raise TEST lthy9
 
@@ -496,7 +516,7 @@
     prod.cases} 
 
   val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = 
-    if get_STEPS lthy > 20
+    if get_STEPS lthy > 26
     then 
       lthy9a    
       |> lift_thms qtys [] alpha_distincts  
@@ -508,7 +528,7 @@
     else raise TEST lthy9a
 
   val (((qsize_eqvt, [qinduct]), qexhausts), lthyB) = 
-    if get_STEPS lthy > 20
+    if get_STEPS lthy > 27
     then
       lthyA 
       |> lift_thms qtys [] raw_size_eqvt

--- a/Nominal/nominal_dt_alpha.ML	Thu Aug 26 02:08:00 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Fri Aug 27 02:03:52 2010 +0800
@@ -110,7 +110,7 @@
      if member (op=) bodies i then [] 
      else [lookup alpha_bn_map bn $ nth args i $ nth args' i]
 
-(* generat the premises for an alpha rule; mk_frees is used
+(* generate the premises for an alpha rule; mk_frees is used
    if no binders are present *)
 fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause =
 let
@@ -626,6 +626,7 @@
   
   val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} 
     @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) 
+
 in
   alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct 
     (K (asm_full_simp_tac ss)) ctxt

--- a/Nominal/nominal_dt_rawfuns.ML	Thu Aug 26 02:08:00 2010 +0800
+++ b/Nominal/nominal_dt_rawfuns.ML	Fri Aug 27 02:03:52 2010 +0800
@@ -62,6 +62,9 @@
 datatype bmode = Lst | Res | Set
 datatype bclause = BC of bmode * (term option * int) list * int list
 
+fun lookup xs x = the (AList.lookup (op=) xs x)
+
+
 (* testing for concrete atom types *)
 fun is_atom ctxt ty =
   Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
@@ -166,7 +169,9 @@
   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)
+    | SOME bn => (to_set (bn $ arg), 
+       if  member (op=) bodies i then @{term "{}::atom set"}  
+       else lookup fv_bn_map bn $ arg)
   end  
 
   val t1 = map (mk_fv_body fv_map args) bodies
@@ -189,7 +194,7 @@
                  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
+    | SOME (SOME bn) => lookup fv_bn_map bn $ arg
   end  
 in
   case bclause of
@@ -201,7 +206,7 @@
 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 fv = lookup 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
@@ -213,7 +218,7 @@
 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 fv_bn = lookup fv_bn_map bn_trm
   val lhs = fv_bn $ list_comb (constr, args)
   val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses
   val rhs = fold_union rhs_trms