381 | exn_message (ERROR_MESSAGE msg) = msg |
381 | exn_message (ERROR_MESSAGE msg) = msg |
382 | exn_message (THEORY (msg, _)) = msg |
382 | exn_message (THEORY (msg, _)) = msg |
383 | exn_message (ProofContext.CONTEXT (msg, _)) = msg |
383 | exn_message (ProofContext.CONTEXT (msg, _)) = msg |
384 | exn_message (Proof.STATE (msg, _)) = msg |
384 | exn_message (Proof.STATE (msg, _)) = msg |
385 | exn_message (ProofHistory.FAIL msg) = msg |
385 | exn_message (ProofHistory.FAIL msg) = msg |
|
386 | exn_message (MetaSimplifier.SIMPROC_FAIL (name, exn)) = |
|
387 fail_message "simproc" ((name, Position.none), exn) |
386 | exn_message (Attrib.ATTRIB_FAIL info) = fail_message "attribute" info |
388 | exn_message (Attrib.ATTRIB_FAIL info) = fail_message "attribute" info |
387 | exn_message (Method.METHOD_FAIL info) = fail_message "method" info |
389 | exn_message (Method.METHOD_FAIL info) = fail_message "method" info |
388 | exn_message (Antiquote.ANTIQUOTE_FAIL info) = fail_message "antiquotation" info |
390 | exn_message (Antiquote.ANTIQUOTE_FAIL info) = fail_message "antiquotation" info |
389 | exn_message (Syntax.AST (msg, _)) = raised_msg "AST" msg |
391 | exn_message (Syntax.AST (msg, _)) = raised_msg "AST" msg |
390 | exn_message (TYPE (msg, _, _)) = raised_msg "TYPE" msg |
392 | exn_message (TYPE (msg, _, _)) = raised_msg "TYPE" msg |