# HG changeset patch
# User wenzelm
# Date 1717666359 -7200
# Node ID 71c1cf9e7413c2e92688798d934f5460585dba76
# Parent  8a0ccdcae2d168365809a4be3885b3dfe3db3b19
tuned signature;

diff -r 8a0ccdcae2d1 -r 71c1cf9e7413 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Wed Jun 05 11:30:26 2024 +0200
+++ b/src/Pure/zterm.ML	Thu Jun 06 11:32:39 2024 +0200
@@ -196,9 +196,11 @@
   | ZBox of serial
   | ZThm of {theory_name: string, thm_name: Thm_Name.T * Position.T, serial: int};
 
+type zproof_const = (zproof_name * zterm) * (ztyp ZTVars.table * zterm ZVars.table);
+
 datatype zproof =
     ZDummy                         (*dummy proof*)
-  | ZConstp of (zproof_name * zterm) * (ztyp ZTVars.table * zterm ZVars.table)
+  | ZConstp of zproof_const
   | ZBoundp of int
   | ZAbst of string * ztyp * zproof
   | ZAbsp of string * zterm * zproof
@@ -217,7 +219,6 @@
   datatype zterm = datatype zterm
   datatype zproof = datatype zproof
   exception ZTERM of string * ztyp list * zterm list * zproof list
-  type zproof_const = (zproof_name * zterm) * (ztyp ZTVars.table * zterm ZVars.table)
   val fold_tvars: (indexname * sort -> 'a -> 'a) -> ztyp -> 'a -> 'a
   val fold_aterms: (zterm -> 'a -> 'a) -> zterm -> 'a -> 'a
   val fold_types: (ztyp -> 'a -> 'a) -> zterm -> 'a -> 'a
@@ -788,8 +789,6 @@
 
 (* constants *)
 
-type zproof_const = (zproof_name * zterm) * (ztyp ZTVars.table * zterm ZVars.table);
-
 fun zproof_const (a, A) : zproof_const =
   let
     val instT =
@@ -802,7 +801,7 @@
         | _ => tab)));
   in ((a, A), (instT, inst)) end;
 
-fun make_const_proof (f, g) (a, insts) =
+fun make_const_proof (f, g) ((a, insts): zproof_const) =
   let
     val typ = subst_type_same (Same.function (fn ((x, _), _) => try f x));
     val term = Same.function (fn ZVar ((x, _), _) => try g x | _ => NONE);