1.1 --- a/test/Tools/isac/Knowledge/biegelinie-3.sml Thu Aug 22 10:27:02 2019 +0200
1.2 +++ b/test/Tools/isac/Knowledge/biegelinie-3.sml Thu Aug 22 11:26:14 2019 +0200
1.3 @@ -91,7 +91,7 @@
1.4 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);
1.5
1.6 Solve.solve m (pt, pos);
1.7 -"~~~~~ fun solve , args:"; val (("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, _)), (pt, (pos as (p, _)))) =
1.8 +"~~~~~ fun solve , args:"; val (("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p, _)))) =
1.9 (m, (pt, pos));
1.10 val {srls, ...} = Specify.get_met mI;
1.11 val itms = case get_obj I pt p of
1.12 @@ -99,7 +99,7 @@
1.13 | _ => error "solve Apply_Method: uncovered case get_obj"
1.14 val thy' = get_obj g_domID pt p;
1.15 val thy = Celem.assoc_thy thy';
1.16 - val (is, env, ctxt, sc) = case Lucin.init_scrstate thy itms mI of
1.17 + val (is, env, ctxt, sc) = case Lucin.init_scrstate ctxt itms mI of
1.18 (is as Istate.ScrState (env,_,_,_,_,_), ctxt, sc) => (is, env, ctxt, sc)
1.19 | _ => error "solve Apply_Method: uncovered case init_scrstate"
1.20 val ini = Lucin.init_form thy sc env;