--- a/Nominal/nominal_dt_alpha.ML	Sat Jul 31 02:05:25 2010 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Sat Jul 31 02:10:42 2010 +0100
@@ -363,30 +363,32 @@
   val true_trms = replicate (length alphas) (K @{term True})
   
   fun apply_all x fs = map (fn f => f x) fs
-  val goal_rhs = 
+  val goals_rhs = 
     group (props @ (alphas ~~ true_trms))
     |> map snd 
     |> map2 apply_all (args1 ~~ args2)
     |> map fold_conj
 
   fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2
-  val goal_lhs = map2 apply_trm_pair alphas (args1 ~~ args2)
+  val goals_lhs = map2 apply_trm_pair alphas (args1 ~~ args2)
 
-  val goal =
-    (map2 (curry HOLogic.mk_imp) goal_lhs goal_rhs)
+  val goals =
+    (map2 (curry HOLogic.mk_imp) goals_lhs goals_rhs)
     |> foldr1 HOLogic.mk_conj
     |> HOLogic.mk_Trueprop
+
+  fun tac ctxt =
+   HEADGOAL 
+     (DETERM o (rtac alpha_induct_thm) 
+      THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt])
 in
-  Goal.prove ctxt' [] [] goal
-    (fn {context, ...} => HEADGOAL 
-      (DETERM o (rtac alpha_induct_thm) THEN_ALL_NEW (rtac @{thm TrueI} ORELSE' cases_tac context)))
+  Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
   |> singleton (ProofContext.export ctxt' ctxt)
   |> Datatype_Aux.split_conj_thm
   |> map (fn th => th RS mp) 
   |> map Datatype_Aux.split_conj_thm
   |> flat
   |> map zero_var_indexes
-  
   |> filter_out (is_true o concl_of)
 end