# HG changeset patch
# User krauss
# Date 1171537331 -3600
# Node ID b8c227d8ca913b20247c87c4242173b7d4047a62
# Parent  b9924abb8c66e937b555c20df890e5ff7804f973
beta_eta_contract specification befor processing. These normal forms avoid unpleasant surprises later on.

diff -r b9924abb8c66 -r b8c227d8ca91 src/HOL/Tools/function_package/mutual.ML
--- 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') =