src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML

 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000"
 ),
  (1, 
-"\000\000\000\000\000\000\000\000\000\142\144\000\000\143\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\142\138\133\000\101\089\088\083\082\081\080\078\077\072\070\057\
+"\000\000\000\000\000\000\000\000\000\143\145\000\000\144\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\143\139\134\000\101\089\088\083\082\081\080\078\077\072\070\057\
 \\048\048\048\048\048\048\048\048\048\048\045\000\039\037\036\033\
 \\030\029\029\029\029\029\029\029\029\029\029\029\029\029\029\029\
 \\029\029\029\029\029\029\029\029\029\029\029\028\000\027\026\000\
 \\000\007\007\023\007\007\020\007\007\013\007\007\007\007\007\007\
 \\007\007\007\007\008\007\007\007\007\007\007\000\006\000\003\000\

 \\100"
 ),
  (101, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\131\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\132\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\131\
 \\000\102\102\128\102\102\124\102\102\118\102\102\108\102\102\102\
 \\102\102\102\102\103\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
  (102, 

 \\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\102\
 \\000\102\102\102\102\102\130\102\102\102\102\102\102\102\102\102\
 \\102\102\102\102\102\102\102\102\102\102\102\000\000\000\000\000\
 \\000"
 ),
- (131, 
-"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\132\132\132\132\132\132\132\132\132\132\132\132\132\132\132\
-\\132\132\132\132\132\132\132\132\132\132\132\000\000\000\000\000\
-\\000"
-),
  (132, 
 "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\132\132\132\132\132\132\132\132\132\132\000\000\000\000\000\000\
-\\000\132\132\132\132\132\132\132\132\132\132\132\132\132\132\132\
-\\132\132\132\132\132\132\132\132\132\132\132\000\000\000\000\132\
-\\000\132\132\132\132\132\132\132\132\132\132\132\132\132\132\132\
-\\132\132\132\132\132\132\132\132\132\132\132\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\133\133\133\133\133\133\133\133\133\133\133\133\133\133\133\
+\\133\133\133\133\133\133\133\133\133\133\133\000\000\000\000\000\
 \\000"
 ),
  (133, 
-"\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\000\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\137\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134"
+"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\133\133\133\133\133\133\133\133\133\133\000\000\000\000\000\000\
+\\000\133\133\133\133\133\133\133\133\133\133\133\133\133\133\133\
+\\133\133\133\133\133\133\133\133\133\133\133\000\000\000\000\133\
+\\000\133\133\133\133\133\133\133\133\133\133\133\133\133\133\133\
+\\133\133\133\133\133\133\133\133\133\133\133\000\000\000\000\000\
+\\000"
 ),
  (134, 
-"\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\136\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\135\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\134\
-\\134"
+"\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\000\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\138\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135"
 ),
  (135, 
-"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\134\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\134\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000"
-),
- (138, 
-"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\141\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\140\139\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000"
-),
- (142, 
-"\000\000\000\000\000\000\000\000\000\142\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\142\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+"\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\137\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\136\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\135\
+\\135"
+),
+ (136, 
+"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\135\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\135\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000"
+),
+ (139, 
+"\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\142\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\141\140\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000"
 ),
  (143, 
-"\000\000\000\000\000\000\000\000\000\000\144\000\000\000\000\000\
+"\000\000\000\000\000\000\000\000\000\143\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\143\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\\000"
+),
+ (144, 
+"\000\000\000\000\000\000\000\000\000\000\145\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
 \\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\

 {fin = [(N 23)], trans = 30},
 {fin = [(N 15)], trans = 0},
 {fin = [(N 12)], trans = 0},
 {fin = [(N 78)], trans = 33},
 {fin = [(N 21)], trans = 0},
-{fin = [(N 303)], trans = 0},
+{fin = [(N 306)], trans = 0},
 {fin = [(N 38)], trans = 0},
 {fin = [(N 31)], trans = 37},
 {fin = [(N 48)], trans = 0},
 {fin = [], trans = 39},
 {fin = [], trans = 40},
 {fin = [(N 68)], trans = 0},
 {fin = [(N 41)], trans = 42},
 {fin = [(N 45)], trans = 0},
-{fin = [(N 297)], trans = 0},
+{fin = [(N 300)], trans = 0},
 {fin = [(N 27)], trans = 45},
 {fin = [(N 36)], trans = 0},
-{fin = [(N 306)], trans = 0},
+{fin = [(N 309)], trans = 0},
 {fin = [(N 126)], trans = 48},
 {fin = [], trans = 49},
 {fin = [(N 104)], trans = 49},
 {fin = [], trans = 51},
 {fin = [(N 119)], trans = 52},

 {fin = [(N 130)], trans = 70},
 {fin = [], trans = 72},
 {fin = [(N 55)], trans = 0},
 {fin = [(N 123)], trans = 74},
 {fin = [(N 58)], trans = 75},
-{fin = [(N 294)], trans = 0},
+{fin = [(N 297)], trans = 0},
 {fin = [(N 29)], trans = 0},
-{fin = [(N 288)], trans = 78},
+{fin = [(N 291)], trans = 78},
 {fin = [(N 76)], trans = 0},
-{fin = [(N 290)], trans = 0},
+{fin = [(N 293)], trans = 0},
 {fin = [(N 82)], trans = 0},
 {fin = [(N 52)], trans = 0},
 {fin = [], trans = 83},
 {fin = [], trans = 84},
 {fin = [], trans = 85},

 {fin = [(N 214),(N 278)], trans = 102},
 {fin = [(N 204),(N 278)], trans = 102},
 {fin = [(N 278)], trans = 128},
 {fin = [(N 278)], trans = 129},
 {fin = [(N 209),(N 278)], trans = 102},
-{fin = [], trans = 131},
-{fin = [(N 286)], trans = 132},
-{fin = [], trans = 133},
+{fin = [(N 281)], trans = 0},
+{fin = [], trans = 132},
+{fin = [(N 289)], trans = 133},
 {fin = [], trans = 134},
 {fin = [], trans = 135},
+{fin = [], trans = 136},
 {fin = [(N 95)], trans = 0},
-{fin = [], trans = 135},
-{fin = [(N 33)], trans = 138},
-{fin = [(N 300)], trans = 0},
+{fin = [], trans = 136},
+{fin = [(N 33)], trans = 139},
+{fin = [(N 303)], trans = 0},
 {fin = [(N 64)], trans = 0},
 {fin = [(N 18)], trans = 0},
-{fin = [(N 2)], trans = 142},
-{fin = [(N 7)], trans = 143},
+{fin = [(N 2)], trans = 143},
+{fin = [(N 7)], trans = 144},
 {fin = [(N 7)], trans = 0}])
 end
 structure StartStates =
 	struct
 	datatype yystartstate = STARTSTATE of int

 | 257 => (col:=yypos-(!eolpos); T.LET_FT(!linep,!col))
 | 265 => (col:=yypos-(!eolpos); T.LET_TT(!linep,!col))
 | 27 => (col:=yypos-(!eolpos); T.COLON(!linep,!col))
 | 271 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.LOWER_WORD(yytext,!linep,!col) end
 | 278 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOLLAR_WORD(yytext,!linep,!col) end
-| 286 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOLLAR_DOLLAR_WORD(yytext,!linep,!col) end
-| 288 => (col:=yypos-(!eolpos); T.PLUS(!linep,!col))
+| 281 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOLLAR_WORD(yytext,!linep,!col) end
+| 289 => let val yytext=yymktext() in col:=yypos-(!eolpos); T.DOLLAR_DOLLAR_WORD(yytext,!linep,!col) end
 | 29 => (col:=yypos-(!eolpos); T.COMMA(!linep,!col))
-| 290 => (col:=yypos-(!eolpos); T.TIMES(!linep,!col))
-| 294 => (col:=yypos-(!eolpos); T.GENTZEN_ARROW(!linep,!col))
-| 297 => (col:=yypos-(!eolpos); T.SUBTYPE(!linep,!col))
-| 300 => (col:=yypos-(!eolpos); T.DEP_PROD(!linep,!col))
-| 303 => (col:=yypos-(!eolpos); T.DEP_SUM(!linep,!col))
-| 306 => (col:=yypos-(!eolpos); T.LET_TERM(!linep,!col))
+| 291 => (col:=yypos-(!eolpos); T.PLUS(!linep,!col))
+| 293 => (col:=yypos-(!eolpos); T.TIMES(!linep,!col))
+| 297 => (col:=yypos-(!eolpos); T.GENTZEN_ARROW(!linep,!col))
+| 300 => (col:=yypos-(!eolpos); T.SUBTYPE(!linep,!col))
+| 303 => (col:=yypos-(!eolpos); T.DEP_PROD(!linep,!col))
+| 306 => (col:=yypos-(!eolpos); T.DEP_SUM(!linep,!col))
+| 309 => (col:=yypos-(!eolpos); T.LET_TERM(!linep,!col))
 | 31 => (col:=yypos-(!eolpos); T.EQUALS(!linep,!col))
 | 33 => (col:=yypos-(!eolpos); T.EXCLAMATION(!linep,!col))
 | 36 => (col:=yypos-(!eolpos); T.LET(!linep,!col))
 | 38 => (col:=yypos-(!eolpos); T.ARROW(!linep,!col))
 | 41 => (col:=yypos-(!eolpos); T.FI(!linep,!col))

  in ( LrTable.NT 80, ( result, LPAREN1left, RPAREN1right), rest671)
 
 end
 |  ( 135, ( ( _, ( MlyValue.atomic_word atomic_word, atomic_word1left,
  atomic_word1right)) :: rest671)) => let val  result = 
-MlyValue.tff_atomic_type (( Atom_type atomic_word ))
+MlyValue.tff_atomic_type (( Atom_type (atomic_word, []) ))
  in ( LrTable.NT 79, ( result, atomic_word1left, atomic_word1right), 
 rest671)
 end
 |  ( 136, ( ( _, ( MlyValue.defined_type defined_type, 
 defined_type1left, defined_type1right)) :: rest671)) => let val  

   | "$i" => Type_Ind
   | "$tType" => Type_Type
   | "$real" => Type_Real
   | "$rat" => Type_Rat
   | "$int" => Type_Int
+  | "$_" => Type_Dummy
   | thing => raise UNRECOGNISED_SYMBOL ("defined_type", thing)
 )
 )
  in ( LrTable.NT 46, ( result, atomic_defined_word1left, 
 atomic_defined_word1right), rest671)

   | "$oType" => TypeSymbol Type_Bool
   | "$int" => TypeSymbol Type_Int
   | "$real" => TypeSymbol Type_Real
   | "$rat" => TypeSymbol Type_Rat
   | "$tType" => TypeSymbol Type_Type
+  | "$_" => TypeSymbol Type_Dummy
 
   | "$true" => Interpreted_Logic True
   | "$false" => Interpreted_Logic False
 
   | "$less" => Interpreted_ExtraLogic Less