Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Proof/proof_rewrite_rules.ML
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)
isabelle