diff -r 8bda1d947df3 -r aa1ba91ed1ff Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Thu Apr 12 01:39:54 2012 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Fri Apr 20 15:28:35 2012 +0200
@@ -29,7 +29,7 @@
   val raw_fv_bn_rsp_aux: Proof.context -> alpha_result -> term list -> term list -> term list -> 
     thm list -> thm list
   val raw_size_rsp_aux: Proof.context -> alpha_result -> thm list -> thm list
-  val raw_constrs_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list
+  val raw_constrs_rsp: Proof.context -> alpha_result -> term list list -> thm list -> thm list list
   val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list
   val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list
   
@@ -749,9 +749,10 @@
       |> Syntax.check_term ctxt
       |> HOLogic.mk_Trueprop
   in
+    map (fn constrs =>
     Goal.prove_multi ctxt [] [] (map prep_goal constrs)
       (K (HEADGOAL 
-        (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps)))
+        (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps)))) constrs
   end