src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML

  in ( LrTable.NT 124, ( result, thf_type_formula1left, 
 thf_type_formula1right), rest671)
 end
 |  ( 22, ( ( _, ( MlyValue.thf_subtype thf_subtype, thf_subtype1left, 
 thf_subtype1right)) :: rest671)) => let val  result = 
-MlyValue.thf_logic_formula (( THF_type thf_subtype ))
+MlyValue.thf_logic_formula (( Type_fmla thf_subtype ))
  in ( LrTable.NT 124, ( result, thf_subtype1left, thf_subtype1right), 
 rest671)
 end
 |  ( 23, ( ( _, ( MlyValue.thf_binary_pair thf_binary_pair, 
 thf_binary_pair1left, thf_binary_pair1right)) :: rest671)) => let val 

  in ( LrTable.NT 123, ( result, thf_binary_tuple1left, 
 thf_binary_tuple1right), rest671)
 end
 |  ( 25, ( ( _, ( MlyValue.thf_binary_type thf_binary_type, 
 thf_binary_type1left, thf_binary_type1right)) :: rest671)) => let val 
- result = MlyValue.thf_binary_formula (( THF_type thf_binary_type ))
+ result = MlyValue.thf_binary_formula (( Type_fmla thf_binary_type ))
  in ( LrTable.NT 123, ( result, thf_binary_type1left, 
 thf_binary_type1right), rest671)
 end
 |  ( 26, ( ( _, ( MlyValue.thf_unitary_formula thf_unitary_formula2, _
 , thf_unitary_formula2right)) :: ( _, ( MlyValue.thf_pair_connective 

 |  ( 121, ( ( _, ( MlyValue.tff_monotype tff_monotype, _, 
 tff_monotype1right)) :: _ :: _ :: ( _, ( MlyValue.tff_variable_list 
 tff_variable_list, _, _)) :: _ :: ( _, ( _, DEP_PROD1left, _)) :: 
 rest671)) => let val  result = MlyValue.tff_quantified_type (
 (
-       Fmla_type (Quant (Dep_Prod, tff_variable_list, THF_type tff_monotype))
+       Fmla_type (Quant (Dep_Prod, tff_variable_list, Type_fmla tff_monotype))
 )
 )
  in ( LrTable.NT 140, ( result, DEP_PROD1left, tff_monotype1right), 
 rest671)
 end

 end
 |  ( 129, ( ( _, ( _, _, RPAREN1right)) :: ( _, ( 
 MlyValue.tff_type_arguments tff_type_arguments, _, _)) :: _ :: ( _, ( 
 MlyValue.atomic_word atomic_word, atomic_word1left, _)) :: rest671))
  => let val  result = MlyValue.tff_atomic_type (
-( Fmla_type (Fmla (Uninterpreted atomic_word, (map THF_type tff_type_arguments))) )
+( Fmla_type (Fmla (Uninterpreted atomic_word, (map Type_fmla tff_type_arguments))) )
 )
  in ( LrTable.NT 79, ( result, atomic_word1left, RPAREN1right), 
 rest671)
 end
 |  ( 130, ( ( _, ( MlyValue.variable_ variable_, variable_1left,