diff -r 5278312037f8 -r f26f00cbd573 src/HOL/TPTP/TPTP_Parser/tptp.yacc
--- a/src/HOL/TPTP/TPTP_Parser/tptp.yacc	Tue Sep 03 21:46:41 2013 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp.yacc	Tue Sep 03 21:46:41 2013 +0100
@@ -183,10 +183,13 @@
   | tptp_file of tptp_problem
   | tptp of tptp_problem
 
-  | thf_let_defn of tptp_let list
+  | thf_let_term_defn of tptp_let
+  | thf_let_formula_defn of tptp_let
   | tff_let of tptp_formula
-  | tff_let_term_defn of tptp_let list
-  | tff_let_formula_defn of tptp_let list
+  | tff_let_term_defn of tptp_let
+  | tff_let_term_binding of tptp_term
+  | tff_let_formula_defn of tptp_let
+  | tff_let_formula_binding of tptp_formula
   | tff_quantified_type of tptp_type
   | tff_monotype of tptp_type
   | tff_type_arguments of tptp_type list
@@ -229,7 +232,7 @@
 
  Parser for TPTP languages. Latest version of the language spec can
  be obtained from http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html
- This implements version 5.3.0.
+ Our parser implements version 5.4.0 of that spec.
 *)
 
 tptp : tptp_file (( tptp_file ))
@@ -333,15 +336,28 @@
   Conditional (thf_logic_formula1, thf_logic_formula2, thf_logic_formula3)
 ))
 
-thf_let : LET_TF LPAREN thf_let_defn COMMA thf_formula RPAREN ((
-  Let (thf_let_defn, thf_formula)
-))
+(*NOTE support for Let in THF is still broken (cf. the spec).
+  When it gets fixed, look at how TFF support is encoded in this file
+  (to possibly replicate some of the checks done there)*)
+thf_let : LET_TF LPAREN thf_let_term_defn COMMA thf_formula RPAREN (( Let (thf_let_term_defn, thf_formula) ))
+        | LET_FF LPAREN thf_let_formula_defn COMMA thf_formula RPAREN (( Let (thf_let_formula_defn, thf_formula) ))
 
-(*FIXME here could check that fmla is of right form (TPTP BNF L130-134)*)
-thf_let_defn : thf_quantified_formula ((
+(*FIXME here could check that fmla is of right form (TPTP BNF (v5.3.0) L130-134)
+  i.e. it should have "=" or "<=>" at the top level.
+  We deviate from the spec by not checking this here, but "Let" support in THF
+  is still not fully specified.
+*)
+thf_let_term_defn : thf_quantified_formula ((
   let
     val (_, vars, fmla) = extract_quant_info thf_quantified_formula
-  in [Let_fmla (hd vars, fmla)]
+  in Let_fmla (vars, fmla)
+  end
+))
+(*NOTE "thf_let_formula_defn" has the same definition as "thf_let_term_defn" (as per the spec)*)
+thf_let_formula_defn : thf_quantified_formula ((
+  let
+    val (_, vars, fmla) = extract_quant_info thf_quantified_formula
+  in Let_fmla (vars, fmla)
   end
 ))
 
@@ -431,21 +447,19 @@
 tff_let : LET_TF LPAREN tff_let_term_defn COMMA tff_formula RPAREN ((Let (tff_let_term_defn, tff_formula) ))
         | LET_FF LPAREN tff_let_formula_defn COMMA tff_formula RPAREN (( Let (tff_let_formula_defn, tff_formula) ))
 
-(*FIXME here could check that fmla is of right form (TPTP BNF L210-214)*)
-(*FIXME why "term" if using "Let_fmla"?*)
-tff_let_term_defn : tff_quantified_formula ((
-  let
-    val (_, vars, fmla) = extract_quant_info tff_quantified_formula
-  in [Let_fmla (hd vars, fmla)]
-  end
+
+tff_let_term_defn : EXCLAMATION LBRKT tff_variable_list RBRKT COLON tff_let_term_binding (( Let_term (tff_variable_list, tff_let_term_binding) ))
+                  | tff_let_term_binding (( Let_term ([], tff_let_term_binding) ))
+
+tff_let_term_binding : term EQUALS term ((
+  Term_Func (Interpreted_ExtraLogic Apply, [term1, term2])
 ))
 
-(*FIXME here could check that fmla is of right form (TPTP BNF L215-217)*)
-tff_let_formula_defn : tff_quantified_formula ((
-  let
-    val (_, vars, fmla) = extract_quant_info tff_quantified_formula
-  in [Let_fmla (hd vars, fmla)]
-  end
+tff_let_formula_defn : EXCLAMATION LBRKT tff_variable_list RBRKT COLON tff_let_formula_binding (( Let_fmla (tff_variable_list, tff_let_formula_binding) ))
+                  | tff_let_formula_binding (( Let_fmla ([], tff_let_formula_binding) ))
+
+tff_let_formula_binding : atomic_formula IFF tff_unitary_formula ((
+  Fmla (Interpreted_Logic Iff, [atomic_formula, tff_unitary_formula])
 ))
 
 tff_sequent : tff_tuple GENTZEN_ARROW tff_tuple (( Sequent (tff_tuple1, tff_tuple2) ))