Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_dt_alpha.ML
changeset 3161 aa1ba91ed1ff
parent 3124 528704b5830e
child 3200 995d47b09ab4 
--- 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
nominal2