test/Tools/isac/Knowledge/biegelinie-3.sml
changeset 59582 23984b62804f
parent 59581 8733ecc08913
child 59583 cfc0dd8b6849
     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;