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\@{AAA_test (unchecked) \aaa_test\}\ -text\bbb_test should fails and trigger an error \ -text*[bbb_test::"'a::one BBB_test"]\\ +text\aaa_test should fail and trigger an error because its type was \<^typ>\'a::one AAA_test\ + in the \<^theory_text>\declare_reference*\ command:\ +(*text*[aaa_test::"'a::one BBB_test"]\\*) text*[aaa_test::"int AAA_test"]\\ -text\bbb_test should fails and trigger an error \ +text\aaa_test' should fail and trigger an error because its type \<^typ>\string AAA_test\ + is not compatible with its type \<^typ>\'a::one AAA_test\ declared in + the \<^theory_text>\declare_reference*\ command:\ text*[aaa_test'::"string AAA_test"]\\