src/Pure/thm.ML

      | _ => err()
   end;
 
 (*Conversion to apply the meta simpset to a term*)
 fun rewritec (prover,signt) (mss as Mss{net,...}) (hypst,t) =
-  let fun rew (t, {thm as Thm{sign,hyps,maxidx,prop,...}, lhs}) =
+  let val t = Pattern.eta_contract t;
+      fun rew {thm as Thm{sign,hyps,maxidx,prop,...}, lhs} =
 	let val unit = if Sign.subsig(sign,signt) then ()
                   else (writeln"Warning: rewrite rule from different theory";
                         raise Pattern.MATCH)
             val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (lhs,t)
             val prop' = subst_vars insts prop;

                  case prover mss thm' of
                    None       => (trace_thm "FAILED" thm'; None)
                  | Some(thm2) => check_conv(thm2,prop'))
         end
 
-      fun rews t =
-        let fun rews1 [] = None
-              | rews1 (rrule::rrules) =
-                  let val opt = rew(t,rrule) handle Pattern.MATCH => None
-                  in case opt of None => rews1 rrules | some => some end;
-        in rews1 end
-
-      fun eta_rews([]) = None
-        | eta_rews(rrules) = rews (Pattern.eta_contract t) rrules
+      fun rews [] = None
+        | rews (rrule::rrules) =
+            let val opt = rew rrule handle Pattern.MATCH => None
+            in case opt of None => rews rrules | some => some end;
 
   in case t of
        Abs(_,_,body) $ u => Some(hypst,subst_bounds([u], body))
-     | _                 => eta_rews(Net.match_term net t)
+     | _                 => rews(Net.match_term net t)
   end;
 
 (*Conversion to apply a congruence rule to a term*)
 fun congc (prover,signt) {thm=cong,lhs=lhs} (hypst,t) =
   let val Thm{sign,hyps,maxidx,prop,...} = cong