The matter turned out quite simple: a literal type constructor name has to be adjusted:
> diff -r eef7af6af2ce thys/Native_Word/Uint32.thy
> --- a/thys/Native_Word/Uint32.thy Thu Mar 03 08:24:04 2016 +0100
> +++ b/thys/Native_Word/Uint32.thy Thu Mar 03 13:13:04 2016 +0100
> @@ -300,7 +300,7 @@
> defines "TR \<equiv> typerep.Typerep" and "bit0 \<equiv> STR
> ''Numeral_Type.bit0''"
> shows
> "term_of_class.term_of x =
> - Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint32.Abs_uint32'')
> (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0
> [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]], TR (STR ''Uint32.uint32'')
> []]))
> + Code_Evaluation.App (Code_Evaluation.Const (STR
> ''Uint32.uint32.Abs_uint32'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR
> bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'')
> []]]]]]], TR (STR ''Uint32.uint32'') []]))
> (term_of_class.term_of (Rep_uint32' x))"
> by(simp add: term_of_anything)
Maybe it is high time for me to provide input syntax CONSTANT ''…'' and
TYPE_CONSTRUCTOR ''…'' for safe references to named entities in HOL.
Hope this helps,
Florian
Am 02.03.2016 um 22:40 schrieb Makarius:
> *** ML ***
>
> * Option ML_exception_debugger controls detailed exception trace via the
> Poly/ML debugger. Relevant ML modules need to be compiled beforehand
> with ML_file_debug, or with ML_file and option ML_debugger enabled. Note
> debugger information requires consirable time and space: main
> Isabelle/HOL with full debugger support may need ML_system_64.
>
>
> This refers to Isabelle/5dfcc9697f29.
>
> Building Pure + HOL with -o ML_debugger requires 40min with 6 cores. It
> is no necessary to compile all ML modules with debugger support, but it
> helps to find the needle in the haystack.
>
>
> Makarius
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
