beta_eta_contract specification befor processing. These normal forms avoid unpleasant surprises later on.

--- a/src/HOL/Tools/function_package/mutual.ML	Wed Feb 14 10:07:17 2007 +0100
+++ b/src/HOL/Tools/function_package/mutual.ML	Thu Feb 15 12:02:11 2007 +0100
@@ -385,7 +385,7 @@
 
 fun prepare_fundef_mutual config defname fixes eqss default lthy =
     let
-      val mutual = analyze_eqs lthy defname (map fst fixes) eqss
+      val mutual = analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss)
       val Mutual {fsum_var=(n, T), qglrs, ...} = mutual
           
       val ((fsum, goalstate, cont), lthy') =