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

Cleanup
ci/woodpecker/push/build Pipeline failed Details

This commit is contained in:
Nicolas Méric 2023-09-20 15:00:43 +02:00
parent c57ce6292b
commit baa36b10c1
1 changed files with 0 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -1299,9 +1299,7 @@ fun elaborate_instances_of thy _ _ term_option _ =
val values = thy |> Proof_Context.init_global |> DOF_core.get_instances
|> Name_Space.dest_table
|> map fst
|> tap (fn is => writeln ("In elaborate_instances_list instances: " ^ \<^make_string> is))
|> f
|> tap (fn is => writeln ("In elaborate_instances_list instances after filter: " ^ \<^make_string> is))
|> map (fn oid => DOF_core.value_of oid thy)
in HOLogic.mk_list class_typ values end
in if equal class_name DOF_core.default_cid