equal
deleted
inserted
replaced
84 |
84 |
85 |
85 |
86 fun HOL_helper1 () = |
86 fun HOL_helper1 () = |
87 let val tp_level = hol_typ_level () |
87 let val tp_level = hol_typ_level () |
88 in |
88 in |
89 case tp_level of T_FULL => full_typed_HOL_helper1 () |
89 case tp_level of T_FULL => (warning "Full type"; full_typed_HOL_helper1 ()) |
90 | T_PARTIAL => partial_typed_HOL_helper1 () |
90 | T_PARTIAL => (warning "Partial type"; partial_typed_HOL_helper1 ()) |
91 | T_CONST => const_typed_HOL_helper1 () |
91 | T_CONST => (warning "Const type"; const_typed_HOL_helper1 ()) |
92 | T_NONE => untyped_HOL_helper1 () |
92 | T_NONE => (warning "Untyped"; untyped_HOL_helper1 ()) |
93 end; |
93 end; |
94 |
94 |
95 |
95 |
96 fun HOL_comb () = |
96 fun HOL_comb () = |
97 let val tp_level = hol_typ_level () |
97 let val tp_level = hol_typ_level () |
98 in |
98 in |
99 case tp_level of T_FULL => full_typed_comb () |
99 case tp_level of T_FULL => (warning "Full type"; full_typed_comb ()) |
100 | T_PARTIAL => partial_typed_comb () |
100 | T_PARTIAL => (warning "Partial type"; partial_typed_comb ()) |
101 | T_CONST => const_typed_comb () |
101 | T_CONST => (warning "Const type"; const_typed_comb ()) |
102 | T_NONE => untyped_comb () |
102 | T_NONE => (warning "Untyped"; untyped_comb ()) |
103 end; |
103 end; |
104 |
104 |
105 |
105 |
106 fun atp_input_file file = |
106 fun atp_input_file file = |
107 let val file' = !ResAtp.problem_name ^ "_" ^ file |
107 let val file' = !ResAtp.problem_name ^ "_" ^ file |