--- a/Nominal/nominal_dt_rawfuns.ML	Thu Jun 03 15:02:52 2010 +0200
+++ b/Nominal/nominal_dt_rawfuns.ML	Mon Jun 07 11:43:01 2010 +0200
@@ -246,6 +246,21 @@
 
 (** equivarance proofs **)
 
+val eqvt_apply_sym = @{thm eqvt_apply[symmetric]}
+
+fun subproof_tac const_names simps = 
+  Subgoal.FOCUS (fn {prems, context, ...} => 
+    HEADGOAL 
+      (simp_tac (HOL_basic_ss addsimps simps)
+       THEN' Nominal_Permeq.eqvt_tac context [] const_names
+       THEN' simp_tac (HOL_basic_ss addsimps (eqvt_apply_sym :: prems))))
+
+fun prove_eqvt_tac insts ind_thms const_names simps ctxt = 
+  HEADGOAL
+    (Object_Logic.full_atomize_tac
+     THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms))  
+     THEN_ALL_NEW  subproof_tac const_names simps ctxt)
+
 fun mk_eqvt_goal pi const arg =
 let
   val lhs = mk_perm pi (const $ arg)
@@ -254,13 +269,6 @@
   HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
 end
 
-fun subproof_tac const_names simps ctxt = 
-  Subgoal.FOCUS (fn {prems, context, ...} => 
-    HEADGOAL 
-      (simp_tac (HOL_basic_ss addsimps simps)
-       THEN' Nominal_Permeq.eqvt_tac context [] const_names
-       THEN' simp_tac (HOL_basic_ss addsimps (@{thms eqvt_apply[symmetric]} @ prems)))) ctxt 
-
 fun raw_prove_eqvt consts ind_thms simps ctxt =
   if null consts then []
   else
@@ -271,18 +279,15 @@
         consts
         |> map fastype_of
         |> map domain_type 
-      val (arg_names, ctxt'') = Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt'
+      val (arg_names, ctxt'') = 
+        Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt'
       val args = map Free (arg_names ~~ arg_tys)
       val goals = map2 (mk_eqvt_goal p) consts args
       val insts = map (single o SOME) arg_names
-      val const_names = map (fst o dest_Const) consts
-
-      fun tac ctxt = 
-        Object_Logic.full_atomize_tac
-        THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms))  
-        THEN_ALL_NEW  subproof_tac const_names simps ctxt 
+      val const_names = map (fst o dest_Const) consts      
     in
-      Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => (HEADGOAL (tac context)))
+      Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => 
+        prove_eqvt_tac insts ind_thms const_names simps context)
       |> ProofContext.export ctxt'' ctxt
     end