--- a/Nominal/nominal_inductive.ML	Thu Jan 06 13:31:44 2011 +0000
+++ b/Nominal/nominal_inductive.ML	Thu Jan 06 14:02:10 2011 +0000
@@ -207,7 +207,7 @@
   by (simp add: permute_plus)}
 
 
-fun binder_tac prem intr_cvars param_trms Ps user_thm avoid avoid_trm concl_args ctxt = 
+fun binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt = 
   Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} =>
     let
       val thy = ProofContext.theory_of ctxt
@@ -274,7 +274,7 @@
 fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args =
   let
     val tac1 = non_binder_tac prem intr_cvars Ps ctxt
-    val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid avoid_trm concl_args ctxt
+    val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt
   in 
     EVERY' [ rtac @{thm allI}, rtac @{thm allI}, if null avoid then tac1 else tac2 ]
   end