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