--- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Mar 04 15:07:34 2005 +0100
@@ -228,7 +228,7 @@
val tvars = term_tvars prop;
val (_, rhs) = Logic.dest_equals prop;
val rhs' = Library.foldl betapply (subst_TVars (map fst tvars ~~ Ts)
- (Library.foldr (fn p => Abs ("", dummyT, abstract_over p)) (vs, rhs)),
+ (foldr (fn p => Abs ("", dummyT, abstract_over p)) rhs vs),
map valOf ts);
in
change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'