[isabelle] Unwanted type annotations



Hi,

For some reason, I can't get Isabelle to print the following term without type annotations:

val t = @{term "0∷'a∷comm_monoid_add"}

I have tried

val ctxt = @{context}
 |> Config.put show_markup                false
 |> Config.put show_types                 false
 |> Config.put show_free_types            false
 |> Config.put show_all_types             false
 |> Config.put show_sorts                 false
val _ = t |> Syntax.string_of_term ctxt |> writeln

which produces the output "0∷'a". Am I doing something wrong?

Best Regards,
Steffen



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.