From 4ad06ce39aef36cee5958d21d9a746a53596d360 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Wed, 4 Nov 2020 14:25:14 +0100 Subject: [PATCH] deactivated class check. --- src/DOF/Isa_COL.thy | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index 1259100..f70ec09 100755 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -95,12 +95,12 @@ fun transform_cid thy NONE X = X |transform_cid thy (SOME cid) (SOME (sub_cid,pos)) = let val cid_long = DOF_core.read_cid_global thy cid val sub_cid_long = DOF_core.read_cid_global thy sub_cid - in if DOF_core.is_subclass_global thy sub_cid_long cid_long + in if DOF_core.is_subclass_global thy sub_cid_long cid_long then (SOME (sub_cid,pos)) else (SOME (sub_cid,pos)) - (* BUG : check does not yet work for - type synonyms. - error("class must be sub-class of "^cid) *) + (* BUG : check reveals problem of Definition* misuse. + error("class "^sub_cid_long^ + " must be sub-class of "^cid_long) *) end in