84 | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts) (*intermed.from specify*) |
84 | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts) (*intermed.from specify*) |
85 | ("end-of-calculation", (ts, _, _)) => ("", ts) |
85 | ("end-of-calculation", (ts, _, _)) => ("", ts) |
86 | ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next" |
86 | ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next" |
87 | _ => raise ERROR "me: uncovered case Step.do_next") |
87 | _ => raise ERROR "me: uncovered case Step.do_next") |
88 val tac = |
88 val tac = |
89 case ts of |
89 case ts of |
90 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end |
90 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end |
91 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac; |
91 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac; |
92 in |
92 in |
93 (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *), |
93 (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *), |
94 tac, Celem.Sundef, pt) |
94 tac, Celem.Sundef, pt) |