Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest
of the error message ("The exception above was raised for...") will appear.
And print_exn calls print_sign_exn_unit so that it can re-raise the SAME
exception.
Pure/Syntax/
This directory contains the source files for Isabelle's syntax module, which
includes a lexer, parser, pretty printer and macro system. Note that only the
following structures are supposed to be exported:
Pretty (generic pretty printing module)
Scanner (generic scanner toolbox)
Syntax (interface to the syntax module)
BasicSyntax (part of Syntax made pervasive)
There is no Makefile to compile these files separately; they are compiled as
part of Pure Isabelle.