From a1677384b36f0d5524f72c3e4c293cff44d8cf09 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Mon, 11 Mar 2024 15:51:34 +0100
Subject: [PATCH] Update bug declare_reference* bug example

---
 Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy b/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy
index 412ee88..3526185 100644
--- a/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy
+++ b/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy
@@ -704,12 +704,15 @@ bbb::"'a list"
 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_test"]\<open>\<close>
+text\<open>aaa_test should fail and trigger an error because its type was \<^typ>\<open>'a::one AAA_test\<close>
+    in the \<^theory_text>\<open>declare_reference*\<close> command:\<close>
+(*text*[aaa_test::"'a::one BBB_test"]\<open>\<close>*)
 
 text*[aaa_test::"int AAA_test"]\<open>\<close>
 
-text\<open>bbb_test should fails and trigger an error \<close>
+text\<open>aaa_test' should fail and trigger an error because its type \<^typ>\<open>string AAA_test\<close>
+    is not compatible with its type  \<^typ>\<open>'a::one AAA_test\<close> declared in
+    the \<^theory_text>\<open>declare_reference*\<close> command:\<close>
 text*[aaa_test'::"string AAA_test"]\<open>\<close>