192 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_')); |
192 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_')); |
193 val (mI, m) = Solve.mk_tac'_ tac; |
193 val (mI, m) = Solve.mk_tac'_ tac; |
194 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*); |
194 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*); |
195 (*if*) member op = Solve.specsteps mI; (*else*) |
195 (*if*) member op = Solve.specsteps mI; (*else*) |
196 |
196 |
197 (*val Updated (cs' as (_, _, (_, p'))) =*) loc_solve_ (mI,m) ptp; |
197 (*val Updated (cs' as (_, _, (_, p'))) =*) loc_solve_ m ptp; |
198 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp); |
198 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp); |
199 |
199 |
200 "~~~~~ fun solve , args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos)); |
200 "~~~~~ fun solve , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos)); |
201 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*) |
201 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*) |
202 val thy' = get_obj g_domID pt (par_pblobj pt p); |
202 val thy' = get_obj g_domID pt (par_pblobj pt p); |
203 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; |
203 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; |
204 val Safe_Step (istate, _, tac) = |
204 val Safe_Step (istate, _, tac) = |
205 (*case*) LucinNEW.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*); |
205 (*case*) LucinNEW.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*); |