diff -r 56b8d977d1c0 -r 34df2cffe259 Nominal/nominal_mutual.ML
--- a/Nominal/nominal_mutual.ML	Tue Mar 15 00:40:39 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Wed Mar 16 20:42:14 2011 +0100
@@ -253,7 +253,7 @@
 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, trsimps, simple_pinducts=[simple_pinduct],
+    val FunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct],
       termination, domintros, ...} = result
 
     val (all_f_defs, fs) =
@@ -270,7 +270,6 @@
 
     val rew_ss = HOL_basic_ss addsimps all_f_defs
     val mpsimps = map2 mk_mpsimp fqgars psimps
-    val mtrsimps = Option.map (map2 mk_mpsimp fqgars) trsimps
     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
@@ -278,7 +277,7 @@
     FunctionResult { fs=fs, G=G, R=R,
       psimps=mpsimps, simple_pinducts=minducts,
       cases=cases, termination=mtermination,
-      domintros=mdomintros, trsimps=mtrsimps}
+      domintros=mdomintros}
   end
 
 (* nominal *)