# HG changeset patch
# User wenzelm
# Date 1724870805 -7200
# Node ID 713424d012fdbc04453c189d02719b80287a5b25
# Parent  3d9e7746d9dbdcfff0814bf927cccb139d41b9c4
proper definition to avoid failure of HOL-Codegenerator_Test (amending 3d9e7746d9db);

diff -r 3d9e7746d9db -r 713424d012fd src/HOL/Library/Open_State_Syntax.thy
--- a/src/HOL/Library/Open_State_Syntax.thy	Wed Aug 28 19:40:07 2024 +0200
+++ b/src/HOL/Library/Open_State_Syntax.thy	Wed Aug 28 20:46:45 2024 +0200
@@ -119,8 +119,7 @@
 
 nonterminal sdo_binds and sdo_bind
 
-definition sdo_syntax :: 'a
-  where "sdo_syntax = undefined"
+definition "sdo_syntax = ()"
 
 syntax
   "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}" [12] 62)