deactivated class check.
This commit is contained in:
parent
da0f3e63f1
commit
4ad06ce39a
|
@ -95,12 +95,12 @@ fun transform_cid thy NONE X = X
|
||||||
|transform_cid thy (SOME cid) (SOME (sub_cid,pos)) =
|
|transform_cid thy (SOME cid) (SOME (sub_cid,pos)) =
|
||||||
let val cid_long = DOF_core.read_cid_global thy cid
|
let val cid_long = DOF_core.read_cid_global thy cid
|
||||||
val sub_cid_long = DOF_core.read_cid_global thy sub_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))
|
then (SOME (sub_cid,pos))
|
||||||
else (SOME (sub_cid,pos))
|
else (SOME (sub_cid,pos))
|
||||||
(* BUG : check does not yet work for
|
(* BUG : check reveals problem of Definition* misuse.
|
||||||
type synonyms.
|
error("class "^sub_cid_long^
|
||||||
error("class must be sub-class of "^cid) *)
|
" must be sub-class of "^cid_long) *)
|
||||||
end
|
end
|
||||||
in
|
in
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue