From 46b094939a7eb4d649b5a9ed97229578b6f5bf5e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Mon, 4 Mar 2024 14:32:46 +0100
Subject: [PATCH] Update bug example in Test_Polymorphic_Classes

---
 Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy b/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy
index 0814421..412ee88 100644
--- a/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy
+++ b/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy
@@ -701,16 +701,16 @@ aaa::"'a list"
 doc_class 'a BBB_test =
 bbb::"'a list"
 
-declare_reference*[aaa_test::"'a::one AAA"]
-text\<open>@{AAA (unchecked) \<open>aaa_test\<close>}\<close>
+declare_reference*[aaa_test::"'a::one AAA_test"]
+text\<open>@{AAA_test (unchecked) \<open>aaa_test\<close>}\<close>
 
 text\<open>bbb_test should fails and trigger an error \<close>
-text*[bbb_test::"'a::one BBB"]\<open>\<close>
+text*[bbb_test::"'a::one BBB_test"]\<open>\<close>
 
-text*[aaa_test::"int AAA"]\<open>\<close>
+text*[aaa_test::"int AAA_test"]\<open>\<close>
 
 text\<open>bbb_test should fails and trigger an error \<close>
-text*[aaa_test'::"string AAA"]\<open>\<close>
+text*[aaa_test'::"string AAA_test"]\<open>\<close>
 
 
 end
\ No newline at end of file