src/Pure/zterm.ML

     ZAxiom of string
   | ZOracle of string
   | 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
   | ZAppt of zproof * zterm
   | ZAppp of zproof * zproof

 sig
   datatype ztyp = datatype ztyp
   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
   val ztyp_ord: ztyp ord
   val fast_zterm_ord: zterm ord

 
 (** proof construction **)
 
 (* constants *)
 
-type zproof_const = (zproof_name * zterm) * (ztyp ZTVars.table * zterm ZVars.table);
-
 fun zproof_const (a, A) : zproof_const =
   let
     val instT =
       ZTVars.build (A |> (fold_types o fold_tvars) (fn v => fn tab =>
         if ZTVars.defined tab v then tab else ZTVars.update (v, ZTVar v) tab));

         (case t of
           ZVar v => if ZVars.defined tab v then tab else ZVars.update (v, t) tab
         | _ => 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);
   in ZConstp (a, Same.commit (map_insts_same typ term) insts) end;