Prepared the code for preservation of bound var names during rewriting. Still
requires a matching function for HO-patterns.
--- a/src/Pure/thm.ML Wed Oct 26 17:41:40 1994 +0100
+++ b/src/Pure/thm.ML Fri Oct 28 10:13:16 1994 +0100
@@ -1169,6 +1169,19 @@
| _ => err()
end;
+(* This code doesn't help at the moment because many bound vars in rewrite
+ rules are eliminated by eta-contraction. Thus the names of bound vars are
+ lost upon rewriting.
+fun ren_inst(insts,prop,pat,obj) =
+ let val ren = match_bvs(pat,obj,[])
+ fun renAbs(Abs(x,T,b)) =
+ Abs(case assoc(ren,x) of None => x | Some(y) => y, T, renAbs(b))
+ | renAbs(f$t) = renAbs(f) $ renAbs(t)
+ | renAbs(t) = t
+ in subst_vars insts (if null(ren) then prop else renAbs(prop)) end;
+*)
+fun ren_inst(insts,prop,_,_) = subst_vars insts prop;
+
(*Conversion to apply the meta simpset to a term*)
fun rewritec (prover,signt) (mss as Mss{net,...}) (hypst,t) =
let val t = Pattern.eta_contract t;
@@ -1178,7 +1191,7 @@
thm;
raise Pattern.MATCH)
val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (lhs,t)
- val prop' = subst_vars insts prop;
+ val prop' = ren_inst(insts,prop,lhs,t);
val hyps' = hyps union hypst;
val thm' = Thm{sign=signt, hyps=hyps', prop=prop', maxidx=maxidx}
val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop')
@@ -1209,7 +1222,7 @@
val tsig = #tsig(Sign.rep_sg signt)
val insts = Pattern.match tsig (lhs,t) handle Pattern.MATCH =>
error("Congruence rule did not match")
- val prop' = subst_vars insts prop;
+ val prop' = ren_inst(insts,prop,lhs,t);
val thm' = Thm{sign=signt, hyps=hyps union hypst,
prop=prop', maxidx=maxidx}
val unit = trace_thm "Applying congruence rule" thm';