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:17 2012 +0100
1.3 @@ -280,11 +280,11 @@
1.4 thf_logic_formula : thf_binary_formula (( thf_binary_formula ))
1.5 | thf_unitary_formula (( thf_unitary_formula ))
1.6 | thf_type_formula (( THF_typing thf_type_formula ))
1.7 - | thf_subtype (( THF_type thf_subtype ))
1.8 + | thf_subtype (( Type_fmla thf_subtype ))
1.9
1.10 thf_binary_formula : thf_binary_pair (( thf_binary_pair ))
1.11 | thf_binary_tuple (( thf_binary_tuple ))
1.12 - | thf_binary_type (( THF_type thf_binary_type ))
1.13 + | thf_binary_type (( Type_fmla thf_binary_type ))
1.14
1.15 thf_binary_pair : thf_unitary_formula thf_pair_connective thf_unitary_formula ((
1.16 Fmla (thf_pair_connective, [thf_unitary_formula1, thf_unitary_formula2])
1.17 @@ -468,7 +468,7 @@
1.18 | tff_quantified_type (( tff_quantified_type ))
1.19
1.20 tff_quantified_type : DEP_PROD LBRKT tff_variable_list RBRKT COLON tff_monotype ((
1.21 - Fmla_type (Quant (Dep_Prod, tff_variable_list, THF_type tff_monotype))
1.22 + Fmla_type (Quant (Dep_Prod, tff_variable_list, Type_fmla tff_monotype))
1.23 ))
1.24 | LPAREN tff_quantified_type RPAREN (( tff_quantified_type ))
1.25
1.26 @@ -480,7 +480,7 @@
1.27
1.28 tff_atomic_type : atomic_word (( Atom_type atomic_word ))
1.29 | defined_type (( Defined_type defined_type ))
1.30 - | atomic_word LPAREN tff_type_arguments RPAREN (( Fmla_type (Fmla (Uninterpreted atomic_word, (map THF_type tff_type_arguments))) ))
1.31 + | atomic_word LPAREN tff_type_arguments RPAREN (( Fmla_type (Fmla (Uninterpreted atomic_word, (map Type_fmla tff_type_arguments))) ))
1.32 | variable_ (( Fmla_type (Pred (Interpreted_ExtraLogic Apply, [Term_Var variable_])) ))
1.33
1.34 tff_type_arguments : tff_atomic_type (( [tff_atomic_type] ))