1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Wed Apr 04 16:29:16 2012 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Wed Apr 04 16:29:17 2012 +0100
     1.3 @@ -53,14 +53,13 @@
     1.4      UMinus | Sum | Difference | Product | Quotient | Quotient_E |
     1.5      Quotient_T | Quotient_F | Remainder_E | Remainder_T | Remainder_F |
     1.6      Floor | Ceiling | Truncate | Round | To_Int | To_Rat | To_Real |
     1.7 -    (*these should be in defined_pred, but that's not being used in TPTP*)
     1.8 +    (*FIXME these should be in defined_pred, but that's not being used in TPTP*)
     1.9      Less | LessEq | Greater | GreaterEq | EvalEq | Is_Int | Is_Rat |
    1.10 -    Distinct |
    1.11 -    Apply (*this is just a matter of convenience*)
    1.12 +    Distinct | Apply
    1.13  
    1.14    and logic_symbol = Equals | NEquals | Or | And | Iff | If | Fi | Xor |
    1.15      Nor | Nand | Not | Op_Forall | Op_Exists |
    1.16 -    (*these should be in defined_pred, but that's not being used in TPTP*)
    1.17 +    (*FIXME these should be in defined_pred, but that's not being used in TPTP*)
    1.18      True | False
    1.19  
    1.20    and quantifier = (*interpreted binders*)
    1.21 @@ -102,7 +101,7 @@
    1.22      | Conditional of tptp_formula * tptp_formula * tptp_formula
    1.23      | Let of tptp_let list * tptp_formula (*FIXME remove list?*)
    1.24      | Atom of tptp_atom
    1.25 -    | THF_type of tptp_type
    1.26 +    | Type_fmla of tptp_type
    1.27      | THF_typing of tptp_formula * tptp_type (*only THF*)
    1.28  
    1.29    and tptp_let =
    1.30 @@ -130,7 +129,8 @@
    1.31    type position = string * int * int
    1.32  
    1.33    datatype tptp_line =
    1.34 -      Annotated_Formula of position * language * string * role * tptp_formula * annotation option
    1.35 +      Annotated_Formula of position * language * string * role *
    1.36 +        tptp_formula * annotation option
    1.37     |  Include of string * string list
    1.38  
    1.39    type tptp_problem = tptp_line list
    1.40 @@ -198,14 +198,12 @@
    1.41      UMinus | Sum | Difference | Product | Quotient | Quotient_E |
    1.42      Quotient_T | Quotient_F | Remainder_E | Remainder_T | Remainder_F |
    1.43      Floor | Ceiling | Truncate | Round | To_Int | To_Rat | To_Real |
    1.44 -    (*these should be in defined_pred, but that's not being used in TPTP*)
    1.45      Less | LessEq | Greater | GreaterEq | EvalEq | Is_Int | Is_Rat |
    1.46      Distinct |
    1.47 -    Apply (*this is just a matter of convenience*)
    1.48 +    Apply
    1.49  
    1.50    and logic_symbol = Equals | NEquals | Or | And | Iff | If | Fi | Xor |
    1.51      Nor | Nand | Not | Op_Forall | Op_Exists |
    1.52 -    (*these should be in defined_pred, but that's not being used in TPTP*)
    1.53      True | False
    1.54  
    1.55    and quantifier = (*interpreted binders*)
    1.56 @@ -247,21 +245,21 @@
    1.57      | Conditional of tptp_formula * tptp_formula * tptp_formula
    1.58      | Let of tptp_let list * tptp_formula
    1.59      | Atom of tptp_atom
    1.60 -    | THF_type of tptp_type
    1.61 +    | Type_fmla of tptp_type
    1.62      | THF_typing of tptp_formula * tptp_type
    1.63  
    1.64    and tptp_let =
    1.65 -      Let_fmla of (string * tptp_type option) * tptp_formula (*both TFF and THF*)
    1.66 -    | Let_term of (string * tptp_type option) * tptp_term  (*only TFF*)
    1.67 +      Let_fmla of (string * tptp_type option) * tptp_formula
    1.68 +    | Let_term of (string * tptp_type option) * tptp_term
    1.69  
    1.70    and tptp_type =
    1.71        Prod_type of tptp_type * tptp_type
    1.72      | Fn_type of tptp_type * tptp_type
    1.73      | Atom_type of string
    1.74      | Defined_type of tptp_base_type
    1.75 -    | Sum_type of tptp_type * tptp_type (*only THF*)
    1.76 -    | Fmla_type of tptp_formula (*only THF*)
    1.77 -    | Subtype of symbol * symbol (*only THF*)
    1.78 +    | Sum_type of tptp_type * tptp_type
    1.79 +    | Fmla_type of tptp_formula
    1.80 +    | Subtype of symbol * symbol
    1.81  
    1.82  type general_list = general_term list
    1.83  type parent_details = general_list
    1.84 @@ -273,13 +271,6 @@
    1.85  
    1.86  exception DEQUOTE of string
    1.87  
    1.88 -(*
    1.89 -datatype defined_functor =
    1.90 -  ITE_T | UMINUS | SUM | DIFFERENCE | PRODUCT | QUOTIENT | QUOTIENT_E |
    1.91 -  QUOTIENT_T | QUOTIENT_F | REMAINDER_E | REMAINDER_T | REMAINDER_F |
    1.92 -  FLOOR | CEILING | TRUNCATE | ROUND | TO_INT | TO_RAT | TO_REAL
    1.93 -*)
    1.94 -
    1.95  type position = string * int * int
    1.96  
    1.97  datatype tptp_line =
    1.98 @@ -474,7 +465,7 @@
    1.99    | string_of_tptp_formula (Conditional _) = "" (*FIXME*)
   1.100    | string_of_tptp_formula (Let _) = "" (*FIXME*)
   1.101    | string_of_tptp_formula (Atom tptp_atom) = string_of_tptp_atom tptp_atom
   1.102 -  | string_of_tptp_formula (THF_type tptp_type) = string_of_tptp_type tptp_type
   1.103 +  | string_of_tptp_formula (Type_fmla tptp_type) = string_of_tptp_type tptp_type
   1.104    | string_of_tptp_formula (THF_typing (tptp_formula, tptp_type)) =
   1.105        string_of_tptp_formula tptp_formula ^ " : " ^ string_of_tptp_type tptp_type
   1.106