--- a/Nominal/nominal_mutual.ML	Mon Jul 18 17:40:13 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Tue Jul 19 01:40:36 2011 +0100
@@ -38,7 +38,6 @@
   fvar : string * typ,
   cargTs: typ list,
   f_def: term,
-
   f: term option,
   f_defthm : thm option}
 
@@ -184,14 +183,13 @@
   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"
-
   in
     Goal.prove ctxt [] []
       (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
@@ -202,6 +200,31 @@
     |> export
   end
 
+fun mk_meqvts ctxt eqvt_thm f_defs =
+  let
+    val ctrm1 = eqvt_thm
+      |> cprop_of
+      |> snd o Thm.dest_implies
+      |> Thm.dest_arg
+      |> Thm.dest_arg1
+      |> Thm.dest_arg
+
+    fun resolve f_def =
+      let
+        val ctrm2 = f_def
+          |> cprop_of
+          |> Thm.dest_equals_lhs
+      in
+        eqvt_thm
+	|> Thm.instantiate (Thm.match (ctrm1, ctrm2))
+        |> simplify (HOL_basic_ss addsimps (@{thm Pair_eqvt} :: @{thms permute_sum.simps}))
+        |> Local_Defs.unfold ctxt [f_def] 
+      end
+  in
+    map resolve f_defs
+  end
+
+
 fun mk_applied_form ctxt caTs thm =
   let
     val thy = ProofContext.theory_of ctxt
@@ -256,14 +279,7 @@
   let
     val result = inner_cont proof
     val NominalFunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct],
-      termination, domintros, eqvts,...} = result
-
-    (*
-    val _ = tracing ("premutual induct:\n" ^ @{make_string} simple_pinduct)
-    val _ = tracing ("premutual termination:\n" ^ @{make_string} termination)
-    val _ = tracing ("premutual psimps:\n" ^ cat_lines (map @{make_string} psimps))
-    val _ = tracing ("premutual eqvts:\n" ^ cat_lines (map @{make_string} eqvts))
-    *)
+      termination, domintros, eqvts=[eqvt],...} = result
 
     val (all_f_defs, fs) =
       map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
@@ -282,17 +298,12 @@
     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 _ = tracing ("postmutual psimps:\n" ^ cat_lines (map @{make_string} mpsimps))
-    val _ = tracing ("postmutual induct:\n" ^ cat_lines (map @{make_string} minducts))
-    val _ = tracing ("postmutual termination:\n" ^ @{make_string} mtermination)
-    *)
-  in
+    val meqvts = mk_meqvts lthy eqvt all_f_defs
+ in
     NominalFunctionResult { fs=fs, G=G, R=R,
       psimps=mpsimps, simple_pinducts=minducts,
       cases=cases, termination=mtermination,
-      domintros=mdomintros, eqvts=eqvts }
+      domintros=mdomintros, eqvts=meqvts }
   end
 
 (* nominal *)