--- a/src/Pure/thm.ML Tue Jan 11 12:58:19 1994 +0100
+++ b/src/Pure/thm.ML Fri Jan 14 08:09:07 1994 +0100
@@ -906,7 +906,8 @@
(*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)
@@ -923,19 +924,14 @@
| 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*)