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