# HG changeset patch
# User wenzelm
# Date 1729456818 -7200
# Node ID 6a33337eb08d895e7d63b02f449584806a1e0edf
# Parent  2fccbfca13618167e951e5fd8b4216c329491f8b
more robust syntax translation;

diff -r 2fccbfca1361 -r 6a33337eb08d src/HOL/Hoare/hoare_syntax.ML
--- a/src/HOL/Hoare/hoare_syntax.ML	Sun Oct 20 22:39:36 2024 +0200
+++ b/src/HOL/Hoare/hoare_syntax.ML	Sun Oct 20 22:40:18 2024 +0200
@@ -97,7 +97,7 @@
           end
       | tr (Const (\<^syntax_const>\<open>_While\<close>,_) $ b $ i $ v $ c) xs =
           let val (c',a) = tr c xs
-              val (v',A) = case v of
+              val (v',A) = case Term_Position.strip_positions v of
                 Const (\<^const_syntax>\<open>HOL.eq\<close>, _) $ z $ t => (t, Syntax_Trans.abs_tr [z, a]) |
                 t => (t, Abs ("n", dummyT, a))
           in (syntax_const ctxt #While $ bexp_tr b xs $ c',