equal
deleted
inserted
replaced
86 let |
86 let |
87 val (chained, extra) = split_used_facts used_facts |
87 val (chained, extra) = split_used_facts used_facts |
88 val (failed, reconstr, ext_time) = |
88 val (failed, reconstr, ext_time) = |
89 case preplay of |
89 case preplay of |
90 Played (reconstr, time) => (false, reconstr, (SOME (false, time))) |
90 Played (reconstr, time) => (false, reconstr, (SOME (false, time))) |
91 | Trust_Playable (reconstr, time) => |
91 | Play_Timed_Out (reconstr, time) => |
92 (false, reconstr, |
92 (false, reconstr, |
93 (case time of |
93 (case time of |
94 NONE => NONE |
94 NONE => NONE |
95 | SOME time => if time = Time.zeroTime then NONE else SOME (true, time))) |
95 | SOME time => if time = Time.zeroTime then NONE else SOME (true, time))) |
96 | Failed_to_Play reconstr => (true, reconstr, NONE) |
96 | Play_Failed reconstr => (true, reconstr, NONE) |
97 val try_line = |
97 val try_line = |
98 ([], map fst extra) |
98 ([], map fst extra) |
99 |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained |
99 |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained |
100 |> (if failed then |
100 |> (if failed then |
101 enclose "One-line proof reconstruction failed: " |
101 enclose "One-line proof reconstruction failed: " |