# HG changeset patch
# User wenzelm
# Date 1636311217 -3600
# Node ID 33ed2eb06d680024c1692b150c7e891e9b9c8c68
# Parent  cc54b8812c63efad4bd56c071e474f2ca8da808f# Parent  ae7edb209706548c3b7b9b45d7ef1a0e66daa2ae
merged

diff -r ae7edb209706 -r 33ed2eb06d68 src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Sun Nov 07 16:35:46 2021 +0100
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Sun Nov 07 19:53:37 2021 +0100
@@ -134,8 +134,8 @@
   assumes "p \<subseteq> i"
       and "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (A n) (i \<inter> {s . v s < n})"
       and "i \<inter> uminus b \<subseteq> q"
-    shows "ValidTC p (While b c) (Awhile i v A) q"
-proof -
+    shows "ValidTC p (While b c) (Awhile i v (\<lambda>n. A n)) q"
+proof -                             
   {
     fix s n
     have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)"
diff -r ae7edb209706 -r 33ed2eb06d68 src/HOL/Hoare/hoare_syntax.ML
--- a/src/HOL/Hoare/hoare_syntax.ML	Sun Nov 07 16:35:46 2021 +0100
+++ b/src/HOL/Hoare/hoare_syntax.ML	Sun Nov 07 19:53:37 2021 +0100
@@ -99,7 +99,7 @@
           let val (c',a) = tr c xs
               val (v',A) = case v of
                 Const (\<^const_syntax>\<open>HOL.eq\<close>, _) $ z $ t => (t, Syntax_Trans.abs_tr [z, a]) |
-                t => (t, absdummy dummyT a)
+                t => (t, Abs ("n", dummyT, a))
           in (syntax_const ctxt #While $ bexp_tr b xs $ c',
               Syntax.const \<^const_syntax>\<open>Awhile\<close>
                 $ assn_tr i xs $ var_tr v' xs $ A)