From d8fde4b4f433606c35a06519117f069c3a0f3e13 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Tue, 19 Apr 2022 14:05:52 +0200
Subject: [PATCH] Cleanup and add test for meta-args for assert*

---
 src/DOF/Isa_DOF.thy      | 10 +---------
 src/tests/Evaluation.thy |  5 ++++-
 2 files changed, 5 insertions(+), 10 deletions(-)

diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy
index d446207..d54a16e 100644
--- a/src/DOF/Isa_DOF.thy
+++ b/src/DOF/Isa_DOF.thy
@@ -1010,8 +1010,6 @@ fun elaborate_instances_list thy isa_name _ _ _ =
     val base_name' = DOF_core.get_class_name_without_prefix (base_name_without_suffix)
     val class_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
                                                 (base_name')
-    val class_list_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
-                                                (base_name' ^ " List.list")
     val tab = #tab(#docobj_tab(DOF_core.get_data_global thy))
     val table_list = Symtab.dest tab
     fun get_instances_name_list _ [] = []
@@ -1028,13 +1026,7 @@ fun elaborate_instances_list thy isa_name _ _ _ =
           end
     val long_class_name = DOF_core.read_cid_global thy base_name'
     val values_list = get_instances_name_list long_class_name table_list
-    val hol_list_terms_list =
-      fold
-        (fn x =>
-         fn y =>
-         Const (@{const_name "Cons"}, [class_typ, class_list_typ] ---> class_list_typ) $ x $ y)
-        values_list (Const (@{const_name "Nil"}, class_list_typ))
-  in hol_list_terms_list end
+  in HOLogic.mk_list class_typ values_list end
 
 fun declare_class_instances_annotation thy doc_class_name =
   let
diff --git a/src/tests/Evaluation.thy b/src/tests/Evaluation.thy
index 7d88a5c..2c7a4c0 100644
--- a/src/tests/Evaluation.thy
+++ b/src/tests/Evaluation.thy
@@ -200,7 +200,10 @@ text\<open>Assertions must be true, hence the error:\<close>
 assert*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>*)
 
 term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
-assert*\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
+assert*[assertionA::A]\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
+
+text-macro*[assertionAA::A]\<open>@{A [display] "assertionA"}\<close> 
+text\<open>... and here we reference @{A [display] \<open>assertionA\<close>}.\<close>
 
 assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>