--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Feb 19 15:57:02 2014 +0000
@@ -528,7 +528,8 @@
| NONE => Free (n, dummyT) (*to infer the variable's type*)
)
| NONE =>
- raise MISINTERPRET_TERM ("Could not type variable", tptp_t))
+ Free (n, dummyT)
+ (*raise MISINTERPRET_TERM ("Could not type variable", tptp_t)*))
else (*variables range over individuals*)
Free (n, interpret_type config thy type_map (Defined_type Type_Ind)),
thy)