From baa36b10c13041a0911f5ec350103e78b4cdf6a3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Wed, 20 Sep 2023 15:00:43 +0200 Subject: [PATCH] Cleanup --- Isabelle_DOF/thys/Isa_DOF.thy | 2 -- 1 file changed, 2 deletions(-) diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index 70a350c..fcbba0c 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -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