--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Tue Mar 25 17:59:34 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Tue Mar 25 19:03:02 2014 +0100
@@ -285,7 +285,7 @@
type tptp_problem = tptp_line list
-fun debug f x = if Options.default_bool @{option exception_trace} then (f x; ()) else ()
+fun debug f x = if Options.default_bool @{option ML_exception_trace} then (f x; ()) else ()
fun nameof_tff_atom_type (Atom_type str) = str
| nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"