379 ip = p; (*false*) |
379 ip = p; (*false*) |
380 member op = [Pbl,Met] p_; (*false*) |
380 member op = [Pbl,Met] p_; (*false*) |
381 "~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip); |
381 "~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip); |
382 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*) |
382 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*) |
383 val thy' = get_obj g_domID pt (par_pblobj pt p); |
383 val thy' = get_obj g_domID pt (par_pblobj pt p); |
384 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
384 val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
385 val (tac_,is,(t,_)) = determine_next_tactic (pt,pos) sc is; (*WAS Empty_Tac_: tac_*) |
385 val (tac_,is,(t,_)) = determine_next_tactic sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*) |
386 case tac_ of Or_to_List' _ => () |
386 case tac_ of Or_to_List' _ => () |
387 | _ => error "Or_to_List broken ?" |
387 | _ => error "Or_to_List broken ?" |
388 |
388 |
389 |
389 |
390 "----------- check thy in CalcTreeTEST ------------------"; |
390 "----------- check thy in CalcTreeTEST ------------------"; |
483 (* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")}, |
483 (* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")}, |
484 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
484 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
485 "~~~~~ fun do_solve_step , args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp); |
485 "~~~~~ fun do_solve_step , args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp); |
486 e_metID = get_obj g_metID pt (par_pblobj pt p) = false; |
486 e_metID = get_obj g_metID pt (par_pblobj pt p) = false; |
487 val thy' = get_obj g_domID pt (par_pblobj pt p); |
487 val thy' = get_obj g_domID pt (par_pblobj pt p); |
488 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
488 val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
489 val (tac_,is,(t,_)) = determine_next_tactic (pt,pos) sc is; |
489 val (tac_,is,(t,_)) = determine_next_tactic sc (pt,pos) ist ctxt; |
490 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*) |
490 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*) |
491 |
491 |
492 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* ) |
492 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* ) |
493 "~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), |
493 "~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), |
494 (sc as Prog (h $ body)), (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is); |
494 (sc as Prog (h $ body)), (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is); |