201 (*loc_solve_ (mI,m) ptp; |
201 (*loc_solve_ (mI,m) ptp; |
202 WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*) |
202 WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*) |
203 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp); |
203 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp); |
204 (*solve m (pt, pos); |
204 (*solve m (pt, pos); |
205 WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*) |
205 WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*) |
206 "~~~~~ fun solve, args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos)); |
206 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos)); |
207 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*); |
207 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*); |
208 val thy' = get_obj g_domID pt (par_pblobj pt p); |
208 val thy' = get_obj g_domID pt (par_pblobj pt p); |
209 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
209 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
210 val d = e_rls; |
210 val d = e_rls; |
211 (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is; |
211 (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is; |