From c3cdcdeec0c00ddb306ab09374abd353097cfbff Mon Sep 17 00:00:00 2001
From: Simon Foster <simondf@gmail.com>
Date: Mon, 6 Jan 2025 11:18:36 +0000
Subject: [PATCH] Removed ghost variable syntax, as it's now in
 Abstract_Prog_Syntax

---
 UTP/ITree_Hoare.thy | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/UTP/ITree_Hoare.thy b/UTP/ITree_Hoare.thy
index 56f6545..23cf949 100644
--- a/UTP/ITree_Hoare.thy
+++ b/UTP/ITree_Hoare.thy
@@ -4,12 +4,6 @@ theory ITree_Hoare
   imports ITree_WP
 begin
 
-syntax
-  "_ghost_old" :: "id" \<comment> \<open> A distinguished name for the ghost state ("old") \<close>
-
-parse_translation \<open> 
-  [(@{syntax_const "_ghost_old"}, fn ctx => fn term => Syntax.free "old")]\<close>
-
 text \<open> We introduce theorem attributed for safe Hoare rules and already proven triples \<close>
 
 named_theorems hoare_safe and hoare_lemmas