Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Update file to match the new name space implementation

This commit is contained in:
Nicolas Méric 2023-02-14 07:09:27 +01:00
parent 1e09598d81
commit 93509ab17d
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/tests/OutOfOrderPresntn.thy
View File

@ -30,9 +30,11 @@ print_doc_items
(* this corresponds to low-level accesses : *) (* this corresponds to low-level accesses : *)
ML\<open> ML\<open>
val docitem_tab = DOF_core.get_instances \<^context> val docitem_tab = DOF_core.get_instances \<^context>
val {docclass_tab, ISA_transformer_tab, ...} val isa_transformer_tab = DOF_core.get_isa_transformers \<^context>
val {docclass_tab, ...}
= DOF_core.get_data @{context}; = DOF_core.get_data @{context};
Name_Space.dest_table docitem_tab; Name_Space.dest_table docitem_tab;
Name_Space.dest_table isa_transformer_tab;
Symtab.dest docclass_tab; Symtab.dest docclass_tab;
app; app;
\<close> \<close>