# HG changeset patch
# User wenzelm
# Date 1702906961 -3600
# Node ID 28342f38da5c365c1e9a6cbec921bc542806c4e2
# Parent  db8ac864ab030d9bff67fe0f0e112ff4e896c661
clarified signature, following Term.subst_bounds_same;

diff -r db8ac864ab03 -r 28342f38da5c src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Mon Dec 18 14:35:11 2023 +0100
+++ b/src/Pure/zterm.ML	Mon Dec 18 14:42:41 2023 +0100
@@ -350,7 +350,7 @@
 
 fun incr_boundvars inc = incr_bv inc 0;
 
-fun subst_bound arg body =
+fun subst_term_bound_same arg =
   let
     fun term lev (ZBound i) =
           if i < lev then raise Same.SAME   (*var is locally bound*)
@@ -361,7 +361,10 @@
           (ZApp (term lev t, Same.commit (term lev) u)
             handle Same.SAME => ZApp (t, term lev u))
       | term _ _ = raise Same.SAME;
-  in Same.commit (term 0) body end;
+  in term end;
+
+fun subst_term_bound arg body =
+  Same.commit (subst_term_bound_same arg 0) body;
 
 
 (* substitution of free or schematic variables *)
@@ -534,10 +537,10 @@
 
 val beta_norm_same =
   let
-    fun norm (ZApp (ZAbs (_, _, body), t)) = subst_bound t body
+    fun norm (ZApp (ZAbs (_, _, body), t)) = subst_term_bound t body
       | norm (ZApp (f, t)) =
           ((case norm f of
-             ZAbs (_, _, body) => subst_bound t body
+             ZAbs (_, _, body) => subst_term_bound t body
            | nf => ZApp (nf, Same.commit norm t))
           handle Same.SAME => ZApp (f, norm t))
       | norm (ZAbs (a, T, t)) = ZAbs (a, T, Same.commit norm t)
@@ -581,10 +584,10 @@
       | norm (ZAbs (a, T, t)) =
           (ZAbs (a, normT T, Same.commit norm t)
             handle Same.SAME => ZAbs (a, T, norm t))
-      | norm (ZApp (ZAbs (_, _, body), t)) = Same.commit norm (subst_bound t body)
+      | norm (ZApp (ZAbs (_, _, body), t)) = Same.commit norm (subst_term_bound t body)
       | norm (ZApp (f, t)) =
           ((case norm f of
-             ZAbs (_, _, body) => Same.commit norm (subst_bound t body)
+             ZAbs (_, _, body) => Same.commit norm (subst_term_bound t body)
            | nf => ZApp (nf, Same.commit norm t))
           handle Same.SAME => ZApp (f, norm t))
       | norm _ = raise Same.SAME;