Dear Frédéric,
> Your previous example works because it is foo which is given to deps_of
> as argument, not the constant C. So one way for calling deps_of with C
> is to replace foo by C:
> export_code C in SML
> (or also by writing @{code C} in ML)
ok, now I can follow your observations.
>
Dear Florian,
Your previous example works because it is foo which is given to deps_of
as argument, not the constant C. So one way for calling deps_of with C
is to replace foo by C:
export_code C in SML
(or also by writing @{code C} in ML)
On the other hand, without knowing if the exportation of
Dear Frédéric,
I cannot follow reproduce observation; using the attached theory in
Isabelle2016-1, I get
> structure Foo : sig
> type 'a b
> type 'a c
> val foo : 'a b -> 'a b
> end = struct
>
> datatype 'a a = A;
>
> datatype 'a b = B of 'a c a
> and 'a c = C of 'a b;
>
> fun foo x =
Dear all,
The SML generated code of the following snippet is not well typed
anymore since Isabelle 2014:
datatype 'a A = aaa
datatype 'a B = bbb "'a C A"
and 'a C = ccc "'a B"
This is because when computing types to be marked as not private (during
the generation of the signature of A, B
