636 then (*if last_elem p = 0 nothing written to pt yet*) (* 2 *) |
636 then (*if last_elem p = 0 nothing written to pt yet*) (* 2 *) |
637 let |
637 let |
638 val metID = get_obj g_metID pt p' |
638 val metID = get_obj g_metID pt p' |
639 val {srls,...} = Specify.get_met metID |
639 val {srls,...} = Specify.get_met metID |
640 in (srls, get_loc pt (p,p_), (#scr o Specify.get_met) metID) end |
640 in (srls, get_loc pt (p,p_), (#scr o Specify.get_met) metID) end |
641 else (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in locate_input_formula, determine_next_tactic*) (* 3 *) |
641 else (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in inform, determine_next_tactic*) (* 3 *) |
642 (Rule.e_rls, get_loc pt (p,p_), |
642 (Rule.e_rls, get_loc pt (p,p_), |
643 case rls' of |
643 case rls' of |
644 Rule.Rls {scr = scr,...} => scr |
644 Rule.Rls {scr = scr,...} => scr |
645 | Rule.Seq {scr = scr,...} => scr |
645 | Rule.Seq {scr = scr,...} => scr |
646 | Rule.Rrls {scr=rfuns,...} => rfuns |
646 | Rule.Rrls {scr=rfuns,...} => rfuns |