Small fix in lifting code for expressions with local variables

isabelle-utp · Feb 24, 2024 · 556985f · 556985f
1 parent 9dc6ace
commit 556985f
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Local_State.thy b/Local_State.thy
@@ -57,6 +57,8 @@ lift_expr_lvar _ trm = trm
 fun lift_lvar n (Const (@{const_name SEXP}, t') $ e)
   = (Const (@{const_name SEXP}, t') $ lift_expr_lvar n e) |
 lift_lvar n (t1 $ t2) = lift_lvar n t1 $ lift_lvar n t2 |
+lift_lvar n (Abs (x, t', trm)) =
+  if x = n then Abs (x, t', trm) else Abs (x, t', lift_lvar n trm) |
 lift_lvar _ trm = trm 
 
 end