--- a/Nominal/nominal_mutual.ML	Tue Jul 19 10:43:43 2011 +0200
+++ b/Nominal/nominal_mutual.ML	Tue Jul 19 19:09:06 2011 +0100
@@ -193,9 +193,56 @@
   in
     Goal.prove ctxt [] []
       (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
-      (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
+      (fn _ => print_tac "start" 
+         THEN (Local_Defs.unfold_tac ctxt all_orig_fdefs)
+         THEN (print_tac "second")
          THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
-         THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *)
+         THEN (print_tac "third")
+         THEN (simp_tac (simpset_of ctxt)) 1
+         THEN (print_tac "fourth")
+      ) (* FIXME: global simpset?!! *)
+    |> restore_cond
+    |> export
+  end
+
+val test1 = @{lemma "x = Inl y ==> permute p (Sum_Type.Projl x) = Sum_Type.Projl (permute p x)" by simp}
+val test2 = @{lemma "x = Inr y ==> permute p (Sum_Type.Projr x) = Sum_Type.Projr (permute p x)" by simp}
+
+fun recover_mutual_eqvt eqvt_thm all_orig_fdefs parts ctxt (fname, _, _, args, rhs)
+  import (export : thm -> thm) sum_psimp_eq =
+  let
+    val (MutualPart {f=SOME f, ...}) = get_part fname parts
+ 
+    val psimp = import sum_psimp_eq
+    val (simp, restore_cond) =
+      case cprems_of psimp of
+        [] => (psimp, I)
+      | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
+      | _ => raise General.Fail "Too many conditions"
+
+    val eqvt_thm' = import eqvt_thm
+    val (simp', restore_cond') =
+      case cprems_of eqvt_thm' of
+        [] => (eqvt_thm, I)
+      | [cond] => (Thm.implies_elim eqvt_thm' (Thm.assume cond), Thm.implies_intr cond)
+      | _ => raise General.Fail "Too many conditions"
+
+    val _ = tracing ("sum_psimp:\n" ^ @{make_string} sum_psimp_eq)
+    val _ = tracing ("psimp:\n" ^ @{make_string} psimp)
+    val _ = tracing ("simp:\n" ^ @{make_string} simp)
+    val _ = tracing ("eqvt:\n" ^ @{make_string} eqvt_thm)
+    
+    val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt		   
+    val p = Free (p, @{typ perm})
+    val ss = HOL_basic_ss addsimps [simp RS test1, simp']
+  in
+    Goal.prove ctxt' [] []
+      (HOLogic.Trueprop $ 
+         HOLogic.mk_eq (mk_perm p (list_comb (f, args)), list_comb (f, map (mk_perm p) args)))
+      (fn _ => print_tac "eqvt start" 
+         THEN (Local_Defs.unfold_tac ctxt all_orig_fdefs)
+         THEN (asm_full_simp_tac ss 1)
+         THEN all_tac) 
     |> restore_cond
     |> export
   end
@@ -295,12 +342,15 @@
     fun mk_mpsimp fqgar sum_psimp =
       in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp
 
+    fun mk_meqvts fqgar sum_psimp =
+      in_context lthy fqgar (recover_mutual_eqvt eqvt all_orig_fdefs parts) sum_psimp
+
     val rew_ss = HOL_basic_ss addsimps all_f_defs
     val mpsimps = map2 mk_mpsimp fqgars psimps
     val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
     val mtermination = full_simplify rew_ss termination
     val mdomintros = Option.map (map (full_simplify rew_ss)) domintros
-    val meqvts = [eqvt] (*mk_meqvts lthy eqvt all_f_defs*)
+    val meqvts = map2 mk_meqvts fqgars psimps
  in
     NominalFunctionResult { fs=fs, G=G, R=R,
       psimps=mpsimps, simple_pinducts=minducts,