# HG changeset patch
# User wenzelm
# Date 1730039400 -3600
# Node ID 41e843d901ee4ae8415ecdf76f953476cd349e3d
# Parent  0eb96012d4160e415479942516f7c4af4f95f739
more robust: avoid non-authentic translations;

diff -r 0eb96012d416 -r 41e843d901ee src/HOL/Bali/State.thy
--- a/src/HOL/Bali/State.thy	Sun Oct 27 12:54:58 2024 +0100
+++ b/src/HOL/Bali/State.thy	Sun Oct 27 15:30:00 2024 +0100
@@ -131,19 +131,15 @@
 subsubsection "object references"
 
 type_synonym oref = "loc + qtname"         \<comment> \<open>generalized object reference\<close>
-syntax
-  Heap  :: "loc   \<Rightarrow> oref"
-  Stat  :: "qtname \<Rightarrow> oref"
-
-syntax_consts
-  Heap == Inl and
-  Stat == Inr
 
 translations
-  "Heap" => "CONST Inl"
-  "Stat" => "CONST Inr"
   (type) "oref" <= (type) "loc + qtname"
 
+abbreviation (input)
+  Heap :: "loc \<Rightarrow> oref" where "Heap \<equiv> Inl"
+abbreviation (input)
+  Stat :: "qtname \<Rightarrow> oref" where "Stat \<equiv> Inr"
+
 definition
   fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool)  \<Rightarrow> (fspec, ty) table" where
   "fields_table G C P =