--- a/Nominal/Nominal2.thy	Wed Dec 22 22:30:43 2010 +0000
+++ b/Nominal/Nominal2.thy	Wed Dec 22 23:12:51 2010 +0000
@@ -44,23 +44,14 @@
   | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1
   | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2
   | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2)  
-*}
 
-ML {*
 fun fold_left f [] z = z
   | fold_left f [x] z = x
   | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z
-*}
 
-ML {*
 fun fold_union_env tys trms = fold_left (mk_union_env tys) trms @{term "{}::atom set"} 
 *}
 
-ML {*
-fold_union_env [] [@{term "t1::atom set"}, @{term "t2::atom set"}, @{term "t3::atom set"}]
-|> Syntax.string_of_term @{context}
-|> writeln
-*}
 
 
 ML {*
@@ -139,6 +130,7 @@
     [] => [] 
   | _ =>
       let
+        val flag = is_recursive_binder bclause
         val binder_trm = comb_binders ctxt bmode parms binders
         val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies)
         val body_ty = fastype_of body_trm
@@ -153,39 +145,34 @@
           | Res => mk_abs @{const_name "Abs_res"} @{typ "atom set"}  @{type_name abs_res}
 
         val abs_lhs = abs_const $ binder_trm $ body_trm
-        val abs_rhs = abs_const $ mk_perm p binder_trm $ mk_perm (Bound 0) body_trm
-        val abs_rhs' = abs_const $ mk_perm (Bound 0) binder_trm $ mk_perm (Bound 0) body_trm
+        val abs_rhs = 
+          if flag
+          then abs_const $ mk_perm p binder_trm $ mk_perm (Bound 0) body_trm
+          else abs_const $ mk_perm (Bound 0) binder_trm $ mk_perm (Bound 0) body_trm
+        
         val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs)
-        val abs_eq' = HOLogic.mk_eq (abs_lhs, abs_rhs')
-        val eq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) 
+        val peq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) 
 
-        val goal = HOLogic.mk_conj (abs_eq, eq)
+        val goal = HOLogic.mk_conj (abs_eq, peq)
           |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t))
           |> HOLogic.mk_Trueprop  
-
-        val goal' = HOLogic.mk_conj (abs_eq', eq)
-          |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t))
-          |> HOLogic.mk_Trueprop   
  
         val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt}
           @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
           fresh_star_set} @ @{thms finite.intros finite_fset}
+  
+        val tac1 = 
+          if flag
+          then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
+          else resolve_tac @{thms Abs_rename_set  Abs_rename_res  Abs_rename_lst}
+        
+        val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss] 
      in
-       if is_recursive_binder bclause
-       then
-         (tracing "recursive";
-         [ Goal.prove ctxt [] [] goal'
-             (K (HEADGOAL (resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
-                 THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss))))
-           |> Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []
-         ])
-       else
-         (tracing "non-recursive";
-         [ Goal.prove ctxt [] [] goal
-             (K (HEADGOAL (resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst}
-                 THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss))))
-           |> Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []
-         ]) 
+       [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2)))
+         |> (if flag
+             then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []
+             else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns [])
+       ]
      end
 *}