# HG changeset patch
# User blanchet
# Date 1403250156 -7200
# Node ID 6907432c47b9cd79315f75091411d0f4ecaef3a5
# Parent  88263522c31eab189ebfa3e4a31ee40317112ef6
made 'tptp_graph' more liberal (why reject TFF?)

diff -r 88263522c31e -r 6907432c47b9 src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML
--- 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.*)