tuned;

--- 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;