equal
deleted
inserted
replaced
123 fun is_typed_hol () = |
123 fun is_typed_hol () = |
124 let val tp_level = hol_typ_level() |
124 let val tp_level = hol_typ_level() |
125 in |
125 in |
126 not (tp_level = ResHolClause.T_NONE) |
126 not (tp_level = ResHolClause.T_NONE) |
127 end; |
127 end; |
128 val include_combS = ResHolClause.include_combS; |
|
129 val include_min_comb = ResHolClause.include_min_comb; |
|
130 |
128 |
131 fun atp_input_file () = |
129 fun atp_input_file () = |
132 let val file = !problem_name |
130 let val file = !problem_name |
133 in |
131 in |
134 if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file)) |
132 if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file)) |