--- a/Nominal/nominal_dt_alpha.ML	Wed Jun 09 15:14:16 2010 +0200
+++ b/Nominal/nominal_dt_alpha.ML	Thu Jun 10 14:53:28 2010 +0200
@@ -401,6 +401,7 @@
 
 (** transitivity proof for alphas **)
 
+(* applies cases rules and resolves them with the last premise *)
 fun ecases_tac cases = 
   Subgoal.FOCUS (fn {prems, ...} =>
     HEADGOAL (resolve_tac cases THEN' rtac (List.last prems)))
@@ -409,6 +410,7 @@
   SUBPROOF (fn {prems, context, ...} =>
     HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems)))
   
+(* instantiates exI with the permutation p + q *)
 val perm_inst_tac =
   Subgoal.FOCUS (fn {params, ...} => 
     let
@@ -425,7 +427,7 @@
 in
   resolve_tac intros
   THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' 
-    TRY o EVERY' 
+    TRY o EVERY'   (* if binders are present *)
       [ etac @{thm exE},
         etac @{thm exE},
         perm_inst_tac ctxt, 
@@ -447,7 +449,7 @@
              ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ])
 end
 
-xfun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) =
+fun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) =
 let
   val lhs = alpha_trm $ arg1 $ arg2
   val mid = alpha_trm $ arg2 $ (Bound 0)