changeset 70417 | eb6ff14767cd |
parent 70412 | 64ead6de6212 |
child 70447 | 755d58b48cec |
--- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Jul 26 14:27:46 2019 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Jul 26 14:43:56 2019 +0200 @@ -243,7 +243,7 @@ (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs), map the ts); in - (Proofterm.change_type (SOME [fastype_of1 (Ts, rhs')]) + (Proofterm.change_types (SOME [fastype_of1 (Ts, rhs')]) Proofterm.reflexive_axm %> rhs', true) end else (prf, false)