> I took the opportunity to have a look at it and found out it can be done
> differently, see attached patch.
The patch is now running on testboard:
> The clue about "integer_of_char" is that it had to work regardless
> whether HOL chars are represented authentic or by target language
> characters (importing "~~/src/HOL/Library/Code_Char").
> Nowadays this can be achieved without spelling out the chars explicitly.
> The last stone to turn around before had been the de-constructivation
> of the char type (b3f2b8c906a6).
Thanks for investigating this.
isabelle-dev mailing list