369 WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*) |
369 WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*) |
370 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp); |
370 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp); |
371 (*solve m (pt, pos); |
371 (*solve m (pt, pos); |
372 WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*) |
372 WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*) |
373 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos)); |
373 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos)); |
374 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*); |
374 Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*); |
375 val thy' = get_obj g_domID pt (par_pblobj pt p); |
375 val thy' = get_obj g_domID pt (par_pblobj pt p); |
376 val (is, sc) = resume_prog thy' (p,p_) pt; |
376 val (is, sc) = resume_prog thy' (p,p_) pt; |
377 val d = Rule_Set.empty; |
377 val d = Rule_Set.empty; |
378 (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is; |
378 (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is; |
379 WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*) |
379 WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*) |