diff -r 84afb941df53 -r d1038e67923a Nominal/nominal_mutual.ML
--- a/Nominal/nominal_mutual.ML	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Mon Jul 18 17:40:13 2011 +0100
@@ -17,7 +17,7 @@
     -> term list
     -> local_theory
     -> ((thm (* goalstate *)
-        * (thm -> Function_Common.function_result) (* proof continuation *)
+        * (thm -> Nominal_Function_Common.nominal_function_result) (* proof continuation *)
        ) * local_theory)
 
 end
@@ -255,8 +255,15 @@
 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
   let
     val result = inner_cont proof
-    val FunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct],
-      termination, domintros, ...} = result
+    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))
+    *)
 
     val (all_f_defs, fs) =
       map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
@@ -275,11 +282,17 @@
     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
-    FunctionResult { fs=fs, G=G, R=R,
+    NominalFunctionResult { fs=fs, G=G, R=R,
       psimps=mpsimps, simple_pinducts=minducts,
       cases=cases, termination=mtermination,
-      domintros=mdomintros}
+      domintros=mdomintros, eqvts=eqvts }
   end
 
 (* nominal *)