1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Wed Apr 04 16:05:52 2012 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Wed Apr 04 16:29:16 2012 +0100
     1.3 @@ -55,6 +55,7 @@
     1.4      Floor | Ceiling | Truncate | Round | To_Int | To_Rat | To_Real |
     1.5      (*these should be in defined_pred, but that's not being used in TPTP*)
     1.6      Less | LessEq | Greater | GreaterEq | EvalEq | Is_Int | Is_Rat |
     1.7 +    Distinct |
     1.8      Apply (*this is just a matter of convenience*)
     1.9  
    1.10    and logic_symbol = Equals | NEquals | Or | And | Iff | If | Fi | Xor |
    1.11 @@ -86,6 +87,7 @@
    1.12      | Term_Conditional of tptp_formula * tptp_term * tptp_term
    1.13      | Term_Num of number_kind * string
    1.14      | Term_Distinct_Object of string
    1.15 +    | Term_Let of tptp_let list * tptp_term (*FIXME remove list?*)
    1.16  
    1.17    and tptp_atom =
    1.18        TFF_Typed_Atom of symbol * tptp_type option (*only TFF*)
    1.19 @@ -98,14 +100,14 @@
    1.20      | Sequent of tptp_formula list * tptp_formula list
    1.21      | Quant of quantifier * (string * tptp_type option) list * tptp_formula
    1.22      | Conditional of tptp_formula * tptp_formula * tptp_formula
    1.23 -    | Let of tptp_let list * tptp_formula
    1.24 +    | Let of tptp_let list * tptp_formula (*FIXME remove list?*)
    1.25      | Atom of tptp_atom
    1.26      | THF_type of tptp_type
    1.27      | THF_typing of tptp_formula * tptp_type (*only THF*)
    1.28  
    1.29    and tptp_let =
    1.30        Let_fmla of (string * tptp_type option) * tptp_formula
    1.31 -    | Let_term of (string * tptp_type option) * tptp_term  (*only TFF*)
    1.32 +    | Let_term of (string * tptp_type option) * tptp_term (*only TFF*)
    1.33  
    1.34    and tptp_type =
    1.35        Prod_type of tptp_type * tptp_type
    1.36 @@ -113,7 +115,7 @@
    1.37      | Atom_type of string
    1.38      | Defined_type of tptp_base_type
    1.39      | Sum_type of tptp_type * tptp_type (*only THF*)
    1.40 -    | Fmla_type of tptp_formula (*only THF*)
    1.41 +    | Fmla_type of tptp_formula
    1.42      | Subtype of symbol * symbol (*only THF*)
    1.43  
    1.44    type general_list = general_term list
    1.45 @@ -198,6 +200,7 @@
    1.46      Floor | Ceiling | Truncate | Round | To_Int | To_Rat | To_Real |
    1.47      (*these should be in defined_pred, but that's not being used in TPTP*)
    1.48      Less | LessEq | Greater | GreaterEq | EvalEq | Is_Int | Is_Rat |
    1.49 +    Distinct |
    1.50      Apply (*this is just a matter of convenience*)
    1.51  
    1.52    and logic_symbol = Equals | NEquals | Or | And | Iff | If | Fi | Xor |
    1.53 @@ -229,6 +232,7 @@
    1.54      | Term_Conditional of tptp_formula * tptp_term * tptp_term
    1.55      | Term_Num of number_kind * string
    1.56      | Term_Distinct_Object of string
    1.57 +    | Term_Let of tptp_let list * tptp_term (*FIXME remove list?*)
    1.58  
    1.59    and tptp_atom =
    1.60        TFF_Typed_Atom of symbol * tptp_type option (*only TFF*)