--- a/Nominal/nominal_mutual.ML	Mon May 09 04:49:58 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Tue May 10 07:47:06 2011 +0100
@@ -118,10 +118,11 @@
     fun convert_eqs (f, qs, gs, args, rhs) =
       let
         val MutualPart {i, i', ...} = get_part f parts
+        val rhs' = rhs
+             |> map_aterms (fn t as Free (n, _) => the_default t (AList.lookup (op =) rews n) | t => t)
       in
         (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
-         SumTree.mk_inj RST n' i' (replace_frees rews rhs)
-         |> Envir.beta_norm)
+         Envir.beta_norm (SumTree.mk_inj RST n' i' rhs'))
       end
 
     val qglrs = map convert_eqs fqgars