# HG changeset patch
# User wenzelm
# Date 1704973467 -3600
# Node ID 9eb9882f184569dd4ef64883e78755ab7508e47b
# Parent  c39aed404ffc80b330b4075122786c88d904c7c9
more thorough treatment of hidden type variables within zproof;

diff -r c39aed404ffc -r 9eb9882f1845 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Thu Jan 11 12:37:10 2024 +0100
+++ b/src/Pure/zterm.ML	Thu Jan 11 12:44:27 2024 +0100
@@ -470,6 +470,26 @@
   subst_term_same typ (Same.function (ZVars.lookup inst));
 
 
+(* fold types/terms within proof *)
+
+fun fold_proof {hyps} typ term =
+  let
+    fun proof ZDummy = I
+      | proof (ZConstp (_, _, instT, inst)) =
+          ZTVars.fold (typ o #2) instT #> ZVars.fold (term o #2) inst
+      | proof (ZBoundp _) = I
+      | proof (ZHyp h) = hyps ? term h
+      | proof (ZAbst (_, T, p)) = typ T #> proof p
+      | proof (ZAbsp (_, t, p)) = term t #> proof p
+      | proof (ZAppt (p, t)) = proof p #> term t
+      | proof (ZAppp (p, q)) = proof p #> proof q
+      | proof (ZClassp (T, _)) = hyps ? typ T;
+  in proof end;
+
+fun fold_proof_types hyps typ =
+  fold_proof hyps typ (fold_types typ);
+
+
 (* map types/terms within proof *)
 
 exception BAD_INST of ((indexname * ztyp) * zterm) list
@@ -830,7 +850,9 @@
   let
     val {zterm, ...} = zterm_cache thy;
 
-    val present_set = Types.build (Types.add_atyps concl #> fold Types.add_atyps hyps);
+    val present_set =
+      Types.build (Types.add_atyps concl #> fold Types.add_atyps hyps #>
+        (fold_proof_types {hyps = true} o fold_tvars) (Types.add_set o typ_of o ZTVar) prf);
     val ucontext as {constraints, outer_constraints, ...} =
       Logic.unconstrain_context [] present_set;