69 val itms = if itms <> [] then itms else I_Model.complete oris probl [] model |
69 val itms = if itms <> [] then itms else I_Model.complete oris probl [] model |
70 val prog_rls = LItool.get_simplifier (pt, pos) |
70 val prog_rls = LItool.get_simplifier (pt, pos) |
71 val (is, env, ctxt, prog) = case LItool.init_pstate prog_rls ctxt itms mI of |
71 val (is, env, ctxt, prog) = case LItool.init_pstate prog_rls ctxt itms mI of |
72 (is as Istate.Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program) |
72 (is as Istate.Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program) |
73 | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate" |
73 | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate" |
74 val ini = LItool.implicit_take prog env; |
74 val ini = LItool.implicit_take ctxt prog env; |
75 val pos = start_new_level pos |
75 val pos = start_new_level pos |
76 val SOME t = (*case*) ini (*of*); |
76 val SOME t = (*case*) ini (*of*); |
77 val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt); |
77 val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt); |
78 val (pos, c, _, pt) = Solve_Step.add show_add (is, ctxt) (pt, pos); |
78 val (pos, c, _, pt) = Solve_Step.add show_add (is, ctxt) (pt, pos); |
79 |
79 |