Translating some HOFs from HasCASL to Isabelle fails

[maeder]

after removing the case expressions in HasCASL/List.het (zip_cons and filter_cons) running Isabelle on 'HasCASL/List_List.thy' (generated by: hets -v2 -o thy HasCASL/List.het) fails with:

*** Type unification failed: Clash of types "Datatype.option" and "List_List.List"
*** Type error in application: Incompatible operand type
***
*** Operator:  op = (map'(h, X_Cons x xs)) :: ??'a List option => bool
*** Operand:
***   unpack2option mapSome
***    (case h x of None => None | Some Xc0 => Some (X_Cons Xc0))
***    (map'(h, xs)) ::
***   ??'a List option option
***
*** The error(s) above occurred in axiom "map_cons"
*** At command "axioms" (line 30 of "/home/maeder/Hets-lib/HasCASL/List_List.thy").

Removing map_cons in List.het, too, works.

Also the commented out sentences in source:trunk/test/HasCASL2IsabelleTests/Hofs.het (i.e. . h1 = h4) fail when run (./run.sh):

*** Type unification failed: Clash of types "Datatype.option" and "Hofs_S.s"
*** Type error in application: Incompatible operand type
***
*** Operator:  op o X_h4 :: ((s => ??'a) => s option => s) => (s => ??'a) ~=> s
*** Operand:   mapSome :: (s => ??'a) => s option ~=> ??'a
***
*** The error(s) above occurred in axiom "Ax15"
*** At command "axioms" (line 30 of "/home/maeder/Hets/test/HasCASL2IsabelleTests/Hofs_S.thy").

The responsible comorphism is source:trunk/Comorphisms/PCoClTyConsHOL2IsabelleHOL.hs