--- a/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML Wed Jun 18 17:42:24 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML Fri Jun 20 09:42:36 2014 +0200
@@ -86,13 +86,11 @@
(*Different styles are applied to nodes relating to clauses written in
difference languages.*)
-exception NO_LANG_STYLE
fun the_lang_style lang =
case lang of
CNF => "dotted"
| FOF => "dashed"
- | THF => "" (*NOTE could use "filled" to contrast with first-order languages*)
- | _ => raise NO_LANG_STYLE
+ | _ => ""
(*Check if the formula just consists of "$false"?
which we interpret to be the last line of the proof.*)