tuned;

--- a/src/Pure/Proof/extraction.ML	Mon Oct 07 21:51:31 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Oct 08 14:27:11 2019 +0200
@@ -116,7 +116,7 @@
 
   in rew end;
 
-val chtypes = Proofterm.change_types o SOME;
+val change_types = Proofterm.change_types o SOME;
 
 fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
 fun corr_name s vs = extr_name s vs ^ "_correctness";
@@ -749,10 +749,10 @@
                       (Abs ("x", T, rlz $ list_comb (Bound 0, args') $ prop));
 
                     val corr_prf' = mkabsp shyps
-                      (chtypes [] Proofterm.equal_elim_axm %> lhs %> rhs %%
-                       (chtypes [propT] Proofterm.symmetric_axm %> rhs %> lhs %%
-                         (chtypes [T, propT] Proofterm.combination_axm %> f %> f %> c %> t' %%
-                           (chtypes [T --> propT] Proofterm.reflexive_axm %> f) %%
+                      (change_types [] Proofterm.equal_elim_axm %> lhs %> rhs %%
+                       (change_types [propT] Proofterm.symmetric_axm %> rhs %> lhs %%
+                         (change_types [T, propT] Proofterm.combination_axm %> f %> f %> c %> t' %%
+                           (change_types [T --> propT] Proofterm.reflexive_axm %> f) %%
                            PAxm (Thm.def_name cname, eqn,
                              SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
                     val corr_prop = Proofterm.prop_of corr_prf';