test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml
changeset 59790 a1944acd8dcf
parent 59765 3ac99a5f910b
child 59791 0db869a16f83
     1.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml	Tue Feb 04 16:45:36 2020 +0100
     1.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml	Tue Feb 04 17:11:54 2020 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4  
     1.5          val Apply_Method mI = (*case*) tac (*of*);
     1.6  (*+*)val (_, (_, _, (pt'''', p''''))) =
     1.7 -           LucinNEW.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) ist_ctxt ptp;
     1.8 +           Lucin.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) ist_ctxt ptp;
     1.9  "~~~~~ fun begin_end_prog , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (ist, ctxt), (pt, pos as (p, _)))
    1.10    = ((Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)), ist_ctxt, ptp);
    1.11        val {ppc, ...} = Specify.get_met mI;
    1.12 @@ -57,10 +57,10 @@
    1.13        val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
    1.14        val thy' = get_obj g_domID pt p;
    1.15        val thy = Celem.assoc_thy thy';
    1.16 -      val srls = Lucin.get_simplifier (pt, pos);
    1.17 +      val srls = LItool.get_simplifier (pt, pos);
    1.18  
    1.19    (*if*) mI = ["Biegelinien", "ausBelastung"] (*else*);
    1.20 -     val (is, env, ctxt, scr) = case Lucin.init_pstate srls ctxt itms mI of
    1.21 +     val (is, env, ctxt, scr) = case LItool.init_pstate srls ctxt itms mI of
    1.22           (is as Istate.Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
    1.23         | _ => error "begin_end_prog Apply_Method': uncovered case init_pstate"
    1.24