tuned comments;

--- a/src/Pure/zterm.ML	Fri Dec 15 17:29:23 2023 +0100
+++ b/src/Pure/zterm.ML	Sun Dec 17 11:15:08 2023 +0100
@@ -362,7 +362,7 @@
   in Same.commit (term 0) body end;
 
 
-(* direct substitution *)
+(* substitution of free or schematic variables *)
 
 fun subst_type_same tvar =
   let
@@ -394,6 +394,9 @@
       | term (ZClass (T, c)) = ZClass (typ T, c);
   in term end;
 
+
+(* map types/terms within proof *)
+
 fun map_insts_same typ term (instT, inst) =
   let
     val changed = Unsynchronized.ref false;