1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp.yacc	Wed Apr 04 16:29:16 2012 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp.yacc	Wed Apr 04 16:29:16 2012 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4    | DUD | INDEF_CHOICE | DEFIN_CHOICE
     1.5    | OPERATOR_FORALL | OPERATOR_EXISTS
     1.6    | PLUS | TIMES | GENTZEN_ARROW | DEP_SUM | DEP_PROD
     1.7 -  | ATOMIC_DEFINED_WORD of string | ATOMIC_SYSTEM_WORD of string
     1.8 +  | DOLLAR_WORD of string | DOLLAR_DOLLAR_WORD of string
     1.9    | SUBTYPE | LET_TERM
    1.10    | THF | TFF | FOF | CNF
    1.11    | ITE_F | ITE_T
    1.12 @@ -191,6 +191,8 @@
    1.13    | tff_monotype of tptp_type
    1.14    | tff_type_arguments of tptp_type list
    1.15    | let_term of tptp_term
    1.16 +  | atomic_defined_word of string
    1.17 +  | atomic_system_word of string
    1.18  
    1.19  %pos int
    1.20  %eop EOF
    1.21 @@ -611,8 +613,8 @@
    1.22  
    1.23  (* Types for THF and TFF *)
    1.24  
    1.25 -defined_type : ATOMIC_DEFINED_WORD ((
    1.26 -  case ATOMIC_DEFINED_WORD of
    1.27 +defined_type : atomic_defined_word ((
    1.28 +  case atomic_defined_word of
    1.29      "$oType" => Type_Bool
    1.30    | "$o" => Type_Bool
    1.31    | "$iType" => Type_Ind
    1.32 @@ -624,7 +626,7 @@
    1.33    | thing => raise UNRECOGNISED_SYMBOL ("defined_type", thing)
    1.34  ))
    1.35  
    1.36 -system_type : ATOMIC_SYSTEM_WORD (( ATOMIC_SYSTEM_WORD ))
    1.37 +system_type : atomic_system_word (( atomic_system_word ))
    1.38  
    1.39  
    1.40  (* First-order atoms *)
    1.41 @@ -641,16 +643,16 @@
    1.42  defined_plain_formula : defined_plain_term (( Pred defined_plain_term ))
    1.43  
    1.44  (*FIXME not used*)
    1.45 -defined_prop : ATOMIC_DEFINED_WORD ((
    1.46 -  case ATOMIC_DEFINED_WORD of
    1.47 +defined_prop : atomic_defined_word ((
    1.48 +  case atomic_defined_word of
    1.49      "$true"  => "$true"
    1.50    | "$false" => "$false"
    1.51    | thing => raise UNRECOGNISED_SYMBOL ("defined_prop", thing)
    1.52  ))
    1.53  
    1.54  (*FIXME not used*)
    1.55 -defined_pred : ATOMIC_DEFINED_WORD ((
    1.56 -  case ATOMIC_DEFINED_WORD of
    1.57 +defined_pred : atomic_defined_word ((
    1.58 +  case atomic_defined_word of
    1.59      "$distinct"  => "$distinct"
    1.60    | "$ite_f" => "$ite_f"
    1.61    | "$less" => "$less"
    1.62 @@ -704,9 +706,9 @@
    1.63  
    1.64  defined_constant : defined_functor (( defined_functor ))
    1.65  
    1.66 -(*FIXME must the ones other than the first batch be included here?*)
    1.67 -defined_functor : ATOMIC_DEFINED_WORD ((
    1.68 -  case ATOMIC_DEFINED_WORD of
    1.69 +(*FIXME would be nicer to split these up*)
    1.70 +defined_functor : atomic_defined_word ((
    1.71 +  case atomic_defined_word of
    1.72      "$uminus" => Interpreted_ExtraLogic UMinus
    1.73    | "$sum" => Interpreted_ExtraLogic Sum
    1.74    | "$difference" => Interpreted_ExtraLogic Difference
    1.75 @@ -757,7 +759,7 @@
    1.76  
    1.77  system_constant : system_functor (( system_functor ))
    1.78  
    1.79 -system_functor : ATOMIC_SYSTEM_WORD (( System ATOMIC_SYSTEM_WORD ))
    1.80 +system_functor : atomic_system_word (( System atomic_system_word ))
    1.81  
    1.82  variable_ : UPPER_WORD  (( UPPER_WORD ))
    1.83  
    1.84 @@ -832,7 +834,6 @@
    1.85  name : atomic_word (( atomic_word ))
    1.86       | integer     (( integer ))
    1.87  
    1.88 -(*FIXME -- "THF" onwards*)
    1.89  atomic_word : LOWER_WORD    (( LOWER_WORD ))
    1.90              | SINGLE_QUOTED (( SINGLE_QUOTED ))
    1.91              | THF           (( "thf" ))
    1.92 @@ -841,7 +842,9 @@
    1.93              | CNF           (( "cnf" ))
    1.94              | INCLUDE       (( "include" ))
    1.95  
    1.96 -(*atomic_defined_word and atomic_system_word are picked up by lex*)
    1.97 +atomic_defined_word : DOLLAR_WORD (( DOLLAR_WORD ))
    1.98 +
    1.99 +atomic_system_word : DOLLAR_DOLLAR_WORD (( DOLLAR_DOLLAR_WORD ))
   1.100  
   1.101  integer: UNSIGNED_INTEGER (( UNSIGNED_INTEGER ))
   1.102         | SIGNED_INTEGER   (( SIGNED_INTEGER ))