1.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml	Sat Mar 07 11:54:13 2020 +0100
     1.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml	Sat Mar 07 14:18:11 2020 +0100
     1.3 @@ -10,8 +10,7 @@
     1.4  "table of contents -----------------------------------------------";
     1.5  "-----------------------------------------------------------------";
     1.6  "-----------------------------------------------------------------";
     1.7 -"-------------- fun get_ctxt -------------------------------------";
     1.8 -"-------------- fun update_ctxt, fun g_ctxt ----------------------";
     1.9 +"-------------- fun get_ctxt, g_ctxt -----------------------------";
    1.10  "-------------- check positions in miniscript --------------------";
    1.11  "-------------- get_allpos' (from ctree above)--------------------";
    1.12  "-------------- cut_level (from ctree above)----------------------";
    1.13 @@ -52,9 +51,9 @@
    1.14  "-----------------------------------------------------------------";
    1.15  
    1.16  
    1.17 -"-------------- fun get_ctxt -------------------------------------";
    1.18 -"-------------- fun get_ctxt -------------------------------------";
    1.19 -"-------------- fun get_ctxt -------------------------------------";
    1.20 +"-------------- fun get_ctxt, g_ctxt -----------------------------";
    1.21 +"-------------- fun get_ctxt, g_ctxt -----------------------------";
    1.22 +"-------------- fun get_ctxt, g_ctxt -----------------------------";
    1.23  val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    1.24  val (dI',pI',mI') =
    1.25    ("Test", ["sqroot-test","univariate","equation","test"],
    1.26 @@ -66,16 +65,10 @@
    1.27  (get_ctxt pt p)
    1.28    handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj";
    1.29  
    1.30 -"-------------- fun update_ctxt, fun g_ctxt ----------------------";
    1.31 -"-------------- fun update_ctxt, fun g_ctxt ----------------------";
    1.32 -"-------------- fun update_ctxt, fun g_ctxt ----------------------";
    1.33  val pt = EmptyPtree;
    1.34  val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term, e_ctxt) pt;
    1.35  val ctxt = get_obj g_ctxt pt [];
    1.36  if is_e_ctxt ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";
    1.37 -val pt = update_ctxt pt [] (Proof_Context.init_global @{theory "Isac_Knowledge"});
    1.38 -if (get_obj g_ctxt pt [] |> Proof_Context.theory_of |> Context.theory_name) = "Isac_Knowledge"
    1.39 -then () else error "--- fun update_ctxt, fun g_ctxt changed";
    1.40  
    1.41  "-------------- check positions in miniscript --------------------";
    1.42  "-------------- check positions in miniscript --------------------";