# HG changeset patch
# User wenzelm
# Date 1702808108 -3600
# Node ID 154166613b40d5462e53140c5870c90f2a2b25d6
# Parent  99a6a831f2c246367939562b73d337376f00d3f5
tuned comments;

diff -r 99a6a831f2c2 -r 154166613b40 src/Pure/zterm.ML
--- 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;