--- a/Nominal/nominal_dt_rawfuns.ML	Wed Jun 02 11:37:51 2010 +0200
+++ b/Nominal/nominal_dt_rawfuns.ML	Thu Jun 03 11:48:44 2010 +0200
@@ -226,9 +226,6 @@
   val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
   val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
 
-  val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) ((flat fv_eqs) @ (flat fv_bn_eqs))))
-
-
   val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
     Function_Common.default_config (pat_completeness_simp constr_thms) lthy
 
@@ -257,6 +254,13 @@
   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
@@ -267,20 +271,18 @@
         consts
         |> map fastype_of
         |> map domain_type 
-      val (arg_names, ctxt'') = Variable.variant_fixes (replicate (length 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' InductTacs.induct_rules_tac ctxt insts ind_thms 
-        THEN_ALL_NEW   
-          (asm_full_simp_tac (HOL_basic_ss addsimps simps)
-           THEN' Nominal_Permeq.eqvt_tac ctxt simps const_names
-           THEN' asm_simp_tac HOL_basic_ss)
+        THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms))  
+        THEN_ALL_NEW  subproof_tac const_names simps ctxt 
     in
-      Goal.prove_multi ctxt' [] [] goals (fn {context, ...} => (HEADGOAL (tac context)))
+      Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => (HEADGOAL (tac context)))
       |> ProofContext.export ctxt'' ctxt
     end