src/Pure/Proof/proof_rewrite_rules.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 15801 d2f5ca3c048d
     1.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -228,7 +228,7 @@
     1.4                val tvars = term_tvars prop;
     1.5                val (_, rhs) = Logic.dest_equals prop;
     1.6                val rhs' = Library.foldl betapply (subst_TVars (map fst tvars ~~ Ts)
     1.7 -                (Library.foldr (fn p => Abs ("", dummyT, abstract_over p)) (vs, rhs)),
     1.8 +                (foldr (fn p => Abs ("", dummyT, abstract_over p)) rhs vs),
     1.9                  map valOf ts);
    1.10              in
    1.11                change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'