# HG changeset patch
# User wenzelm
# Date 1703067399 -3600
# Node ID 140c7fac037aa43b4ac3ef8a9eebb8945c866064
# Parent  de58e518ed61ed8870dc7554fc9ac81185115274
tuned;

diff -r de58e518ed61 -r 140c7fac037a src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Tue Dec 19 23:06:26 2023 +0100
+++ b/src/Pure/zterm.ML	Wed Dec 20 11:16:39 2023 +0100
@@ -746,7 +746,7 @@
         | _ => tab)));
   in (a, A, instT, inst) end;
 
-fun make_const_proof (f, g) ((a, A, instT, inst): zproof_const) =
+fun make_const_proof (f, g) (a, A, instT, inst) =
   let
     val instT' = ZTVars.map (fn ((x, _), _) => fn y => the_default y (try f x)) instT;
     val inst' = ZVars.map (fn ((x, _), _) => fn y => the_default y (try g x)) inst;