1.1 --- a/test/Tools/isac/Knowledge/rateq.sml	Sat Feb 04 17:00:25 2023 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/rateq.sml	Tue Feb 07 17:25:09 2023 +0100
     1.3 @@ -129,17 +129,17 @@
     1.4  UnparseC.term @{context} tm = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
     1.5  (*                                     ------ \<up> ----- ? "x" ?*)
     1.6  "~~~~~ to check_leaf return val:"; val ((Program.Tac stac, a')) = ((Program.Tac (subst_atomic E t), NONE));
     1.7 -val stac' = eval_prog_expr (ThyC.get_theory thy) prog_rls (subst_atomic (upd_env_opt E (a,v)) stac);
     1.8 +val stac' = eval_prog_expr (ThyC.get_theory @{context} thy) prog_rls (subst_atomic (upd_env_opt E (a,v)) stac);
     1.9  UnparseC.term @{context} stac' = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
    1.10  "~~~~~ to scan_dn return val:"; val ((a', Program.Tac stac)) = ((a', Program.Tac stac'));
    1.11 -val m = LItool.tac_from_prog pt (ThyC.get_theory th) stac;
    1.12 +val m = LItool.tac_from_prog pt (ThyC.get_theory @{context} th) stac;
    1.13  case m of Check_elementwise "Assumptions" => () | _ => (); (*m' = Empty_Tac_ ???!??? *);
    1.14  val (p''''', pt''''', m''''') = (p, pt, m);
    1.15  "~~~~~ fun check , args:"; val ((p,p_), pt, (m as Check_elementwise pred)) = (p, pt, m);
    1.16  member op = [Pbl,Met] p_; (* = false*)
    1.17          val pp = par_pblobj pt p; 
    1.18          val thy' = (get_obj g_domID pt pp):theory';
    1.19 -        val thy = ThyC.get_theory thy'
    1.20 +        val thy = ThyC.get_theory @{context} thy'
    1.21          val metID = (get_obj g_metID pt pp)
    1.22          val {crls,...} =  MethodC.from_store ctxt metID
    1.23          val (f,asm) = case p_ of Frm => (get_obj g_form pt p , [])