# HG changeset patch
# User wenzelm
# Date 1701946263 -3600
# Node ID 377260b2824df207441073c2d65396d217861742
# Parent  4affbdbeefd459cb9e8955630523bc7bcd05c031
clarified signature: more standard argument order;

diff -r 4affbdbeefd4 -r 377260b2824d src/Provers/blast.ML
--- a/src/Provers/blast.ML	Thu Dec 07 11:48:34 2023 +0100
+++ b/src/Provers/blast.ML	Thu Dec 07 11:51:03 2023 +0100
@@ -251,13 +251,16 @@
 (*increment a term's non-local bound variables
      inc is  increment for bound variables
      lev is  level at which a bound variable is considered 'loose'*)
-fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
-  | incr_bv (inc, lev, Abs(a,body)) = Abs(a, incr_bv(inc,lev+1,body))
-  | incr_bv (inc, lev, f$t) = incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
-  | incr_bv (inc, lev, u) = u;
+fun incr_bv inc =
+  let
+    fun term lev (t as Bound i) = if i >= lev then Bound (i + inc) else t
+      | term lev (Abs (a, t)) = Abs (a, term (lev + 1) t)
+      | term lev (t $ u) = term lev t $ term lev u
+      | term _ t = t;
+  in term end;
 
 fun incr_boundvars  0  t = t
-  | incr_boundvars inc t = incr_bv(inc,0,t);
+  | incr_boundvars inc t = incr_bv inc 0 t;
 
 
 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.