merged

--- a/src/HOL/Proofs/ex/XML_Data.thy	Thu Jul 18 16:00:40 2024 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Thu Jul 18 17:02:39 2024 +0200
@@ -14,11 +14,11 @@
 ML \<open>
   fun export_proof thy thm = thm
     |> Proof_Syntax.standard_proof_of {full = true, expand_name = Thm.expand_name thm}
-    |> Proofterm.encode (Sign.consts_of thy);
+    |> Proofterm.encode thy;
 
   fun import_proof thy xml =
     let
-      val prf = Proofterm.decode (Sign.consts_of thy) xml;
+      val prf = Proofterm.decode thy xml;
       val (prf', _) = Proofterm.freeze_thaw_prf prf;
     in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end;
 \<close>

--- a/src/Pure/Build/export_theory.ML	Thu Jul 18 16:00:40 2024 +0200
+++ b/src/Pure/Build/export_theory.ML	Thu Jul 18 17:02:39 2024 +0200
@@ -310,7 +310,7 @@
         (prop, deps, proof) |>
           let
             open XML.Encode Term_XML.Encode;
-            val encode_proof = Proofterm.encode_standard_proof consts;
+            val encode_proof = Proofterm.encode_standard_proof thy;
           in triple encode_prop (list Thm_Name.encode) encode_proof end
       end;
 

--- a/src/Pure/General/table.ML	Thu Jul 18 16:00:40 2024 +0200
+++ b/src/Pure/General/table.ML	Thu Jul 18 17:02:39 2024 +0200
@@ -66,7 +66,8 @@
   val insert_set: key -> set -> set
   val remove_set: key -> set -> set
   val make_set: key list -> set
-  val unsynchronized_cache: (key -> 'a) -> key -> 'a
+  type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int}
+  val unsynchronized_cache: (key -> 'a) -> 'a cache_ops
 end;
 
 functor Table(Key: KEY): TABLE =
@@ -591,12 +592,13 @@
 
 (* cache *)
 
+type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int};
+
 fun unsynchronized_cache f =
   let
     val cache1 = Unsynchronized.ref empty;
     val cache2 = Unsynchronized.ref empty;
-  in
-    fn x =>
+    fun apply x =
       (case lookup (! cache1) x of
         SOME y => y
       | NONE =>
@@ -605,8 +607,10 @@
           | NONE =>
               (case Exn.result f x of
                 Exn.Res y => (Unsynchronized.change cache1 (update (x, y)); y)
-              | Exn.Exn exn => (Unsynchronized.change cache2 (update (x, exn)); Exn.reraise exn))))
-  end;
+              | Exn.Exn exn => (Unsynchronized.change cache2 (update (x, exn)); Exn.reraise exn))));
+    fun reset () = (cache2 := empty; cache1 := empty);
+    fun total_size () = size (! cache1) + size (! cache2);
+  in {apply = apply, reset = reset, size = total_size} end;
 
 
 (* ML pretty-printing *)

--- a/src/Pure/proofterm.ML	Thu Jul 18 16:00:40 2024 +0200
+++ b/src/Pure/proofterm.ML	Thu Jul 18 17:02:39 2024 +0200
@@ -65,12 +65,13 @@
   val no_thm_proofs: proof -> proof
   val no_body_proofs: proof -> proof
 
-  val encode: Consts.T -> proof XML.Encode.T
-  val encode_body: Consts.T -> proof_body XML.Encode.T
-  val encode_standard_term: Consts.T -> term XML.Encode.T
-  val encode_standard_proof: Consts.T -> proof XML.Encode.T
-  val decode: Consts.T -> proof XML.Decode.T
-  val decode_body: Consts.T -> proof_body XML.Decode.T
+  val proof_to_zproof: theory -> proof -> zproof
+  val encode_standard_term: theory -> term XML.Encode.T
+  val encode_standard_proof: theory -> proof XML.Encode.T
+  val encode: theory -> proof XML.Encode.T
+  val encode_body: theory -> proof_body XML.Encode.T
+  val decode: theory -> proof XML.Decode.T
+  val decode_body: theory -> proof_body XML.Decode.T
 
   val %> : proof * term -> proof
 
@@ -369,6 +370,40 @@
 
 (** XML data representation **)
 
+(* encode as zterm/zproof *)
+
+fun proof_to_zproof thy =
+  let
+    val {ztyp, zterm} = ZTerm.zterm_cache thy;
+    val ztvar = ztyp #> (fn ZTVar v => v);
+
+    fun zproof_const name prop typargs =
+      let
+        val vs = rev ((fold_types o fold_atyps) (insert (op =) o ztvar) prop []);
+        val Ts = map ztyp typargs
+      in ZConstp ((name, zterm prop), (ZTVars.make (vs ~~ Ts), ZVars.empty)) end;
+
+    fun zproof MinProof = ZNop
+      | zproof (PBound i) = ZBoundp i
+      | zproof (Abst (a, SOME T, p)) = ZAbst (a, ztyp T, zproof p)
+      | zproof (AbsP (a, SOME t, p)) = ZAbsp (a, zterm t, zproof p)
+      | zproof (p % SOME t) = ZAppt (zproof p, zterm t)
+      | zproof (p %% q) = ZAppp (zproof p, zproof q)
+      | zproof (Hyp t) = ZHyp (zterm t)
+      | zproof (PAxm (a, prop, SOME Ts)) = zproof_const (ZAxiom a) prop Ts
+      | zproof (PClass (T, c)) = OFCLASSp (ztyp T, c)
+      | zproof (Oracle (a, prop, SOME Ts)) = zproof_const (ZOracle a) prop Ts
+      | zproof (PThm ({serial, pos, theory_name, thm_name, prop, types = SOME Ts, ...}, _)) =
+          let
+            val name = (thm_name, try hd pos |> the_default Position.none);
+            val proof_name = ZThm {theory_name = theory_name, thm_name = name, serial = serial};
+          in zproof_const proof_name prop Ts end;
+  in zproof end;
+
+fun encode_standard_term thy = ZTerm.zterm_of thy #> ZTerm.encode_zterm {typed_vars = false};
+fun encode_standard_proof thy = proof_to_zproof thy #> ZTerm.encode_zproof {typed_vars = false};
+
+
 (* encode *)
 
 local
@@ -399,39 +434,10 @@
     (a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
       (Future.join (thm_node_body thm_node))))));
 
-fun standard_term consts t = t |> variant
- [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))),
-  fn Free (a, _) => ([a], []),
-  fn Var (a, _) => (indexname a, []),
-  fn Bound a => ([], int a),
-  fn Abs (a, b, c) => ([a], pair typ (standard_term consts) (b, c)),
-  fn t as op $ a =>
-    if can Logic.match_of_class t then raise Match
-    else ([], pair (standard_term consts) (standard_term consts) a),
-  fn t =>
-    let val (T, c) = Logic.match_of_class t
-    in ([c], typ T) end];
-
-fun standard_proof consts prf = prf |> variant
- [fn MinProof => ([], []),
-  fn PBound a => ([], int a),
-  fn Abst (a, SOME b, c) => ([a], pair typ (standard_proof consts) (b, c)),
-  fn AbsP (a, SOME b, c) => ([a], pair (standard_term consts) (standard_proof consts) (b, c)),
-  fn a % SOME b => ([], pair (standard_proof consts) (standard_term consts) (a, b)),
-  fn a %% b => ([], pair (standard_proof consts) (standard_proof consts) (a, b)),
-  fn Hyp a => ([], standard_term consts a),
-  fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
-  fn PClass (T, c) => ([c], typ T),
-  fn Oracle (name, prop, SOME Ts) => ([name], pair (standard_term consts) (list typ) (prop, Ts)),
-  fn PThm ({serial, theory_name, thm_name, types = SOME Ts, ...}, _) =>
-    ([int_atom serial, theory_name, #1 thm_name, int_atom (#2 thm_name)], list typ Ts)];
-
 in
 
-val encode = proof;
-val encode_body = proof_body;
-val encode_standard_term = standard_term;
-val encode_standard_proof = standard_proof;
+val encode = proof o Sign.consts_of;
+val encode_body = proof_body o Sign.consts_of;
 
 end;
 
@@ -473,8 +479,8 @@
 
 in
 
-val decode = proof;
-val decode_body = proof_body;
+val decode = proof o Sign.consts_of;
+val decode_body = proof_body o Sign.consts_of;
 
 end;
 
@@ -2160,13 +2166,12 @@
     val args = [] |> add_standard_vars_term prop' |> add_standard_vars prf' |> rev;
     val typargs = [] |> Term.add_tfrees prop' |> fold_proof_terms Term.add_tfrees prf' |> rev;
 
-    val consts = Sign.consts_of thy;
     val xml = (typargs, (args, (prop', no_thm_names prf'))) |>
       let
         open XML.Encode Term_XML.Encode;
         val encode_vars = list (pair string typ);
-        val encode_term = encode_standard_term consts;
-        val encode_proof = encode_standard_proof consts;
+        val encode_term = encode_standard_term thy;
+        val encode_proof = encode_standard_proof thy;
       in pair (list (pair string sort)) (pair encode_vars (pair encode_term encode_proof)) end;
   in
     Export.export_params (Context.Theory thy)

--- a/src/Pure/term_items.ML	Thu Jul 18 16:00:40 2024 +0200
+++ b/src/Pure/term_items.ML	Thu Jul 18 17:02:39 2024 +0200
@@ -34,7 +34,8 @@
   val make1: key * 'a -> 'a table
   val make2: key * 'a -> key * 'a -> 'a table
   val make3: key * 'a -> key * 'a -> key * 'a -> 'a table
-  val unsynchronized_cache: (key -> 'a) -> key -> 'a
+  type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int};
+  val unsynchronized_cache: (key -> 'a) -> 'a cache_ops
   type set = int table
   val add_set: key -> set -> set
   val make_set: key list -> set
@@ -86,6 +87,7 @@
 fun make2 e1 e2 = build (add e1 #> add e2);
 fun make3 e1 e2 e3 = build (add e1 #> add e2 #> add e3);
 
+type 'a cache_ops = 'a Table.cache_ops;
 val unsynchronized_cache = Table.unsynchronized_cache;
 
 

--- a/src/Pure/thm.ML	Thu Jul 18 16:00:40 2024 +0200
+++ b/src/Pure/thm.ML	Thu Jul 18 17:02:39 2024 +0200
@@ -1100,8 +1100,8 @@
                 SOME T' => T'
               | NONE => raise Fail "strip_shyps: bad type variable in proof term"));
         val map_ztyp =
-          ZTypes.unsynchronized_cache
-            (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar));
+          #apply (ZTypes.unsynchronized_cache
+            (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar)));
 
         val zproof' = ZTerm.map_proof_types {hyps = true} map_ztyp zproof;
         val proof' = Proofterm.map_proof_types (Term.map_atyps_same map_atyp) proof;

--- a/src/Pure/zterm.ML	Thu Jul 18 16:00:40 2024 +0200
+++ b/src/Pure/zterm.ML	Thu Jul 18 17:02:39 2024 +0200
@@ -251,10 +251,15 @@
   val map_proof_types: {hyps: bool} -> ztyp Same.operation -> zproof -> zproof
   val map_class_proof: (ztyp * class, zproof) Same.function -> zproof -> zproof
   val ztyp_of: typ -> ztyp
+  val ztyp_dummy: ztyp
+  val typ_of_tvar: indexname * sort -> typ
+  val typ_of: ztyp -> typ
+  val reset_cache: theory -> theory
+  val check_cache: theory -> {ztyp: int, typ: int} option
+  val ztyp_cache: theory -> typ -> ztyp
+  val typ_cache: theory -> ztyp -> typ
   val zterm_cache: theory -> {zterm: term -> zterm, ztyp: typ -> ztyp}
   val zterm_of: theory -> term -> zterm
-  val typ_of_tvar: indexname * sort -> typ
-  val typ_of: ztyp -> typ
   val term_of: theory -> zterm -> term
   val beta_norm_term_same: zterm Same.operation
   val beta_norm_proof_same: zproof Same.operation
@@ -262,7 +267,7 @@
   val beta_norm_term: zterm -> zterm
   val beta_norm_proof: zproof -> zproof
   val beta_norm_prooft: zproof -> zproof
-  val norm_type: Type.tyenv -> ztyp -> ztyp
+  val norm_type: theory -> Type.tyenv -> ztyp -> ztyp
   val norm_term: theory -> Envir.env -> zterm -> zterm
   val norm_proof: theory -> Envir.env -> term list -> zproof -> zproof
   val zproof_const_typargs: zproof_const -> ((indexname * sort) * ztyp) list
@@ -310,6 +315,9 @@
   val of_sort_proof: Sorts.algebra -> sorts_proof -> (typ * class -> zproof) ->
     typ * sort -> zproof list
   val unconstrainT_proof: theory -> sorts_proof -> Logic.unconstrain_context -> zproof -> zproof
+  val encode_ztyp: ztyp XML.Encode.T
+  val encode_zterm: {typed_vars: bool} -> zterm XML.Encode.T
+  val encode_zproof: {typed_vars: bool} -> zproof XML.Encode.T
 end;
 
 structure ZTerm: ZTERM =
@@ -470,7 +478,7 @@
 
 fun instantiate_type_same instT =
   if ZTVars.is_empty instT then Same.same
-  else ZTypes.unsynchronized_cache (subst_type_same (Same.function (ZTVars.lookup instT)));
+  else #apply (ZTypes.unsynchronized_cache (subst_type_same (Same.function (ZTVars.lookup instT))));
 
 fun instantiate_term_same typ inst =
   subst_term_same typ (Same.function (ZVars.lookup inst));
@@ -577,7 +585,7 @@
   in Same.commit proof end;
 
 
-(* convert ztyp / zterm vs. regular typ / term *)
+(* convert ztyp vs. regular typ *)
 
 fun ztyp_of (TFree (a, S)) = ZTVar ((a, ~1), S)
   | ztyp_of (TVar v) = ZTVar v
@@ -587,13 +595,75 @@
   | ztyp_of (Type (c, [T])) = ZType1 (c, ztyp_of T)
   | ztyp_of (Type (c, ts)) = ZType (c, map ztyp_of ts);
 
-fun ztyp_cache () = Typtab.unsynchronized_cache ztyp_of;
+val ztyp_dummy = ztyp_of dummyT;
+
+fun typ_of_tvar ((a, ~1), S) = TFree (a, S)
+  | typ_of_tvar v = TVar v;
+
+fun typ_of (ZTVar v) = typ_of_tvar v
+  | typ_of (ZFun (T, U)) = typ_of T --> typ_of U
+  | typ_of ZProp = propT
+  | typ_of (ZType0 c) = Type (c, [])
+  | typ_of (ZType1 (c, T)) = Type (c, [typ_of T])
+  | typ_of (ZType (c, Ts)) = Type (c, map typ_of Ts);
+
+
+(* cache within theory context *)
+
+local
+
+structure Data = Theory_Data
+(
+  type T = (ztyp Typtab.cache_ops * typ ZTypes.cache_ops) option;
+  val empty = NONE;
+  val merge = K NONE;
+);
+
+fun make_ztyp_cache () = Typtab.unsynchronized_cache ztyp_of;
+fun make_typ_cache () = ZTypes.unsynchronized_cache typ_of;
+
+fun init_cache thy =
+  if is_some (Data.get thy) then NONE
+  else SOME (Data.put (SOME (make_ztyp_cache (), make_typ_cache ())) thy);
+
+fun exit_cache thy =
+  (case Data.get thy of
+    SOME (cache1, cache2) => (#reset cache1 (); #reset cache2 (); SOME (Data.put NONE thy))
+  | NONE => NONE);
+
+in
+
+val _ = Theory.setup (Theory.at_begin init_cache #> Theory.at_end exit_cache);
+
+fun reset_cache thy =
+  (case Data.get thy of
+    SOME (cache1, cache2) => (#reset cache1 (); #reset cache2 (); thy)
+  | NONE => thy);
+
+fun check_cache thy =
+  Data.get thy
+  |> Option.map (fn (cache1, cache2) => {ztyp = #size cache1 (), typ = #size cache2 ()});
+
+fun ztyp_cache thy =
+  (case Data.get thy of
+    SOME (cache, _) => cache
+  | NONE => make_ztyp_cache ()) |> #apply;
+
+fun typ_cache thy =
+  (case Data.get thy of
+    SOME (_, cache) => cache
+  | NONE => make_typ_cache ()) |> #apply;
+
+end;
+
+
+(* convert zterm vs. regular term *)
 
 fun zterm_cache thy =
   let
     val typargs = Consts.typargs (Sign.consts_of thy);
 
-    val ztyp = ztyp_cache ();
+    val ztyp = ztyp_cache thy;
 
     fun zterm (Free (x, T)) = ZVar ((x, ~1), ztyp T)
       | zterm (Var (xi, T)) = ZVar (xi, ztyp T)
@@ -612,18 +682,6 @@
 
 val zterm_of = #zterm o zterm_cache;
 
-fun typ_of_tvar ((a, ~1), S) = TFree (a, S)
-  | typ_of_tvar v = TVar v;
-
-fun typ_of (ZTVar v) = typ_of_tvar v
-  | typ_of (ZFun (T, U)) = typ_of T --> typ_of U
-  | typ_of ZProp = propT
-  | typ_of (ZType0 c) = Type (c, [])
-  | typ_of (ZType1 (c, T)) = Type (c, [typ_of T])
-  | typ_of (ZType (c, Ts)) = Type (c, map typ_of Ts);
-
-fun typ_cache () = ZTypes.unsynchronized_cache typ_of;
-
 fun term_of thy =
   let
     val instance = Consts.instance (Sign.consts_of thy);
@@ -717,11 +775,13 @@
         | norm (ZType (a, Ts)) = ZType (a, Same.map norm Ts);
     in norm end;
 
-fun norm_term_same {ztyp, zterm, typ} (envir as Envir.Envir {tyenv, tenv, ...}) =
+fun norm_term_same {ztyp, zterm} (envir as Envir.Envir {tyenv, tenv, ...}) =
   let
     val lookup =
       if Vartab.is_empty tenv then K NONE
-      else ZVars.unsynchronized_cache (apsnd typ #> Envir.lookup envir #> Option.map zterm);
+      else
+        #apply (ZVars.unsynchronized_cache
+          (apsnd typ_of #> Envir.lookup envir #> Option.map zterm));
 
     val normT = norm_type_same ztyp tyenv;
 
@@ -776,15 +836,9 @@
         in beta_norm_prooft (map_proof {hyps = false} inst_typ norm_term prf) end
   end;
 
-fun norm_cache thy =
-  let
-    val {ztyp, zterm} = zterm_cache thy;
-    val typ = typ_cache ();
-  in {ztyp = ztyp, zterm = zterm, typ = typ} end;
-
-fun norm_type tyenv = Same.commit (norm_type_same (ztyp_cache ()) tyenv);
-fun norm_term thy envir = Same.commit (norm_term_same (norm_cache thy) envir);
-fun norm_proof thy envir = norm_proof_cache (norm_cache thy) envir;
+fun norm_type thy tyenv = Same.commit (norm_type_same (ztyp_cache thy) tyenv);
+fun norm_term thy envir = Same.commit (norm_term_same (zterm_cache thy) envir);
+fun norm_proof thy envir = norm_proof_cache (zterm_cache thy) envir;
 
 
 
@@ -870,7 +924,8 @@
     val typ_operation = #typ_operation ucontext {strip_sorts = true};
     val unconstrain_typ = Same.commit typ_operation;
     val unconstrain_ztyp =
-      ZTypes.unsynchronized_cache (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of));
+      #apply (ZTypes.unsynchronized_cache
+        (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of)));
     val unconstrain_zterm = zterm o Term.map_types typ_operation;
     val unconstrain_proof = Same.commit (map_proof_types {hyps = true} unconstrain_ztyp);
 
@@ -1087,10 +1142,10 @@
     val typ =
       if Names.is_empty tfrees then Same.same
       else
-        ZTypes.unsynchronized_cache
+        #apply (ZTypes.unsynchronized_cache
           (subst_type_same (fn ((a, i), S) =>
             if i = ~1 andalso Names.defined tfrees a then ZTVar ((a, idx), S)
-            else raise Same.SAME));
+            else raise Same.SAME)));
     val term =
       subst_term_same typ (fn ((x, i), T) =>
         if i = ~1 andalso Names.defined frees x then ZVar ((x, idx), T)
@@ -1112,10 +1167,10 @@
     let
       val tab = ZTVars.build (names |> fold (fn ((a, S), b) => ZTVars.add (((a, ~1), S), b)));
       val typ =
-        ZTypes.unsynchronized_cache (subst_type_same (fn v =>
+        #apply (ZTypes.unsynchronized_cache (subst_type_same (fn v =>
           (case ZTVars.lookup tab v of
             NONE => raise Same.SAME
-          | SOME w => ZTVar w)));
+          | SOME w => ZTVar w))));
     in map_proof_types {hyps = false} typ prf end;
 
 fun legacy_freezeT_proof t prf =
@@ -1124,7 +1179,7 @@
   | SOME f =>
       let
         val tvar = ztyp_of o Same.function f;
-        val typ = ZTypes.unsynchronized_cache (subst_type_same tvar);
+        val typ = #apply (ZTypes.unsynchronized_cache (subst_type_same tvar));
       in map_proof_types {hyps = false} typ prf end);
 
 
@@ -1158,7 +1213,7 @@
   if inc = 0 then Same.same
   else
     let fun tvar ((a, i), S) = if i >= 0 then ZTVar ((a, i + inc), S) else raise Same.SAME
-    in ZTypes.unsynchronized_cache (subst_type_same tvar) end;
+    in #apply (ZTypes.unsynchronized_cache (subst_type_same tvar)) end;
 
 fun incr_indexes_proof inc prf =
   let
@@ -1240,7 +1295,7 @@
 
 fun assumption_proof thy envir Bs Bi n visible prf =
   let
-    val cache as {zterm, ...} = norm_cache thy;
+    val cache as {zterm, ...} = zterm_cache thy;
     val normt = zterm #> Same.commit (norm_term_same cache envir);
   in
     ZAbsps (map normt Bs)
@@ -1258,7 +1313,7 @@
 
 fun bicompose_proof thy env smax flatten Bs As A oldAs n m visible rprf sprf =
   let
-    val cache as {zterm, ...} = norm_cache thy;
+    val cache as {zterm, ...} = zterm_cache thy;
     val normt = zterm #> Same.commit (norm_term_same cache env);
     val normp = norm_proof_cache cache env visible;
 
@@ -1292,12 +1347,14 @@
 
 fun unconstrainT_proof thy sorts_proof (ucontext: Logic.unconstrain_context) =
   let
-    val cache = norm_cache thy;
     val algebra = Sign.classes_of thy;
 
+    val cache = zterm_cache thy;
+    val typ_cache = typ_cache thy;
+
     val typ =
-      ZTypes.unsynchronized_cache
-        (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of);
+      #apply (ZTypes.unsynchronized_cache
+        (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of));
 
     val typ_sort = #typ_operation ucontext {strip_sorts = false};
 
@@ -1307,11 +1364,67 @@
       | NONE => raise Fail "unconstrainT_proof: missing constraint");
 
     fun class (T, c) =
-      let val T' = Same.commit typ_sort (#typ cache T)
+      let val T' = Same.commit typ_sort (typ_cache T)
       in the_single (of_sort_proof algebra sorts_proof hyps (T', [c])) end;
   in
     map_proof_types {hyps = false} typ #> map_class_proof class #> beta_norm_prooft
     #> fold_rev (implies_intr_proof' o #zterm cache o #2) (#constraints ucontext)
   end;
 
+
+
+(** XML data representation **)
+
+(* encode *)
+
+local
+
+open XML.Encode Term_XML.Encode;
+
+fun ztyp T = T |> variant
+ [fn ZFun args => (["fun"], pair ztyp ztyp args)
+   | ZProp => (["prop"], [])
+   | ZType0 a => ([a], [])
+   | ZType1 (a, b) => ([a], list ztyp [b])
+   | ZType (a, b) => ([a], list ztyp b),
+  fn ZTVar ((a, ~1), b) => ([a], sort b),
+  fn ZTVar (a, b) => (indexname a, sort b)];
+
+fun zvar_type {typed_vars} T =
+  if typed_vars andalso T <> ztyp_dummy then ztyp T else [];
+
+fun zterm flag t = t |> variant
+ [fn ZConst0 a => ([a], [])
+   | ZConst1 (a, b) => ([a], list ztyp [b])
+   | ZConst (a, b) => ([a], list ztyp b),
+  fn ZVar ((a, ~1), b) => ([a], zvar_type flag b),
+  fn ZVar (a, b) => (indexname a, zvar_type flag b),
+  fn ZBound a => ([], int a),
+  fn ZAbs (a, b, c) => ([a], pair ztyp (zterm flag) (b, c)),
+  fn ZApp a => ([], pair (zterm flag) (zterm flag) a),
+  fn OFCLASS (a, b) => ([b], ztyp a)];
+
+fun zproof flag prf = prf |> variant
+ [fn ZNop => ([], []),
+  fn ZBoundp a => ([], int a),
+  fn ZAbst (a, b, c) => ([a], pair ztyp (zproof flag) (b, c)),
+  fn ZAbsp (a, b, c) => ([a], pair (zterm flag) (zproof flag) (b, c)),
+  fn ZAppt a => ([], pair (zproof flag) (zterm flag) a),
+  fn ZAppp a => ([], pair (zproof flag) (zproof flag) a),
+  fn ZHyp a => ([], zterm flag a),
+  fn ZConstp (c as ((ZAxiom a, b), _)) => ([a], list (ztyp o #2) (zproof_const_typargs c)),
+  fn OFCLASSp (a, b) => ([b], ztyp a),
+  fn ZConstp (c as ((ZOracle a, b), _)) => ([a], list (ztyp o #2) (zproof_const_typargs c)),
+  fn ZConstp (c as ((ZThm {theory_name, thm_name = (name, _), serial}, b), _)) =>
+    ([int_atom serial, theory_name, #1 name, int_atom (#2 name)],
+      list (ztyp o #2) (zproof_const_typargs c))];
+
+in
+
+val encode_ztyp = ztyp;
+val encode_zterm = zterm;
+val encode_zproof = zproof;
+
 end;
+
+end;
\ No newline at end of file