equal
deleted
inserted
replaced
95 tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl]))) |
95 tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl]))) |
96 end |
96 end |
97 |
97 |
98 fun take_time timeout tac arg = |
98 fun take_time timeout tac arg = |
99 let val timing = Timing.start () in |
99 let val timing = Timing.start () in |
100 (TimeLimit.timeLimit timeout tac arg; Played (#cpu (Timing.result timing))) |
100 (Timeout.apply timeout tac arg; Played (#cpu (Timing.result timing))) |
101 handle TimeLimit.TimeOut => Play_Timed_Out timeout |
101 handle Timeout.TIMEOUT _ => Play_Timed_Out timeout |
102 end |
102 end |
103 |
103 |
104 fun resolve_fact_names ctxt names = |
104 fun resolve_fact_names ctxt names = |
105 (names |
105 (names |
106 |>> map string_of_label |
106 |>> map string_of_label |