equal
deleted
inserted
replaced
271 |
271 |
272 val specialize_type = ATP_Util.specialize_type |
272 val specialize_type = ATP_Util.specialize_type |
273 val eta_expand = ATP_Util.eta_expand |
273 val eta_expand = ATP_Util.eta_expand |
274 |
274 |
275 fun DETERM_TIMEOUT delay tac st = |
275 fun DETERM_TIMEOUT delay tac st = |
276 Seq.of_list (the_list (TimeLimit.timeLimit delay (fn () => SINGLE tac st) ())) |
276 Seq.of_list (the_list (Timeout.apply delay (fn () => SINGLE tac st) ())) |
277 |
277 |
278 val indent_size = 2 |
278 val indent_size = 2 |
279 |
279 |
280 val maybe_quote = ATP_Util.maybe_quote |
280 val maybe_quote = ATP_Util.maybe_quote |
281 |
281 |