1.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml	Tue Aug 16 14:47:05 2022 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml	Tue Aug 16 15:53:20 2022 +0200
     1.3 @@ -79,3 +79,4 @@
     1.4  case nxt of Model_Problem => ()
     1.5  | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem";
     1.6  
     1.7 +(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Isac_Knowledge"*)

     2.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml	Tue Aug 16 14:47:05 2022 +0200
     2.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml	Tue Aug 16 15:53:20 2022 +0200
     2.3 @@ -64,4 +64,6 @@
     2.4  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_,Add_Given "equality (x + 1 = 2)*)
     2.5  val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = (_,Add_Given "solveFor x"*)
     2.6  case nxt of (Add_Given "solveFor x") => ()
     2.7 -| _ => error "minisubpbl: Add_Given is broken in root-problem";
     2.8 \ No newline at end of file
     2.9 +| _ => error "minisubpbl: Add_Given is broken in root-problem";
    2.10 +
    2.11 +(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)

     3.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml	Tue Aug 16 14:47:05 2022 +0200
     3.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml	Tue Aug 16 15:53:20 2022 +0200
     3.3 @@ -94,3 +94,5 @@
     3.4  then case tac of Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") => ()
     3.5    | _ => error "Minisubplb/200-start-method-NEXT_STEP.sml CHANGED 1"
     3.6  else error "Minisubplb/200-start-method-NEXT_STEP.sml CHANGED 2"
     3.7 +
     3.8 +(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)

     4.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Tue Aug 16 14:47:05 2022 +0200
     4.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Tue Aug 16 15:53:20 2022 +0200
     4.3 @@ -234,3 +234,5 @@
     4.4      (Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])) => ()
     4.5    | _ => error "Minisubpbl/250-Rewrite_Set-from-method changed 1"
     4.6  else error "Minisubpbl/250-Rewrite_Set-from-method changed 2";
     4.7 +
     4.8 +(*ctxt* )Proof_Context.theory_of (Ctree.get_ctxt pt p);( *ctxt CANNOT BE RETRIEVED*)

     5.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml	Tue Aug 16 14:47:05 2022 +0200
     5.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml	Tue Aug 16 15:53:20 2022 +0200
     5.3 @@ -57,4 +57,7 @@
     5.4      if pr_ctree pr_short pt = ".    ----- pblobj -----\n1.   x + 1 = 2\n" then ()
     5.5      else error "Apply_Method [Test, squ-equ-test-subpbl1] changed pt"
     5.6      ) else error "Apply_Method [Test, squ-equ-test-subpbl1] changed p") 
     5.7 -| _ => error "Apply_Method [Test, squ-equ-test-subpbl1] changed tac"
     5.8 +| _ => error "Apply_Method [Test, squ-equ-test-subpbl1] changed tac";
     5.9 +
    5.10 +(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
    5.11 +

     6.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Tue Aug 16 14:47:05 2022 +0200
     6.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Tue Aug 16 15:53:20 2022 +0200
     6.3 @@ -84,3 +84,5 @@
     6.4  if p = ([3, 1], Frm) andalso f2str f = "- 1 + x = 0" andalso
     6.5    Tactic.input_to_string nxt = "Rewrite_Set_Inst ([(''bdv'', x)], \"isolate_bdv\")"
     6.6  then () else error "Minisubpbl/400-start-meth-subpbl changed";
     6.7 +
     6.8 +(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)

     7.1 --- a/test/Tools/isac/Minisubpbl/450-Rewrite_Set_Inst.sml	Tue Aug 16 14:47:05 2022 +0200
     7.2 +++ b/test/Tools/isac/Minisubpbl/450-Rewrite_Set_Inst.sml	Tue Aug 16 15:53:20 2022 +0200
     7.3 @@ -32,3 +32,5 @@
     7.4  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*);
     7.5  case nxt of (Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")) => ()
     7.6  | _ => error "Rewrite_Set_Inst changed";
     7.7 +
     7.8 +(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)

     8.1 --- a/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml	Tue Aug 16 14:47:05 2022 +0200
     8.2 +++ b/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml	Tue Aug 16 15:53:20 2022 +0200
     8.3 @@ -98,3 +98,4 @@
     8.4  (*+*)  map UnparseC.term asm = []
     8.5  (*+*)then () else error "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml CHANGED";
     8.6  
     8.7 +(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)

     9.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml	Tue Aug 16 14:47:05 2022 +0200
     9.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml	Tue Aug 16 15:53:20 2022 +0200
     9.3 @@ -84,4 +84,7 @@
     9.4  
     9.5  val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["LINEAR", "uval (is, sc) = resume_prog thy' (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *);
     9.6  case nxt of ( Check_Postcond ["LINEAR", "univariate", "equation", "test"]) => ()
     9.7 -| _ => error "450-nxt-Check_Postcond broken"
     9.8 +| _ => error "450-nxt-Check_Postcond broken";
     9.9 +
    9.10 +(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
    9.11 +

    10.1 --- a/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml	Tue Aug 16 14:47:05 2022 +0200
    10.2 +++ b/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml	Tue Aug 16 15:53:20 2022 +0200
    10.3 @@ -40,3 +40,4 @@
    10.4  case nxt of (Check_elementwise "Assumptions") => ()
    10.5  | _ => error "Check_elementwise changed; after switch sub-->root-method";
    10.6  
    10.7 +(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)

    11.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml	Tue Aug 16 14:47:05 2022 +0200
    11.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml	Tue Aug 16 15:53:20 2022 +0200
    11.3 @@ -96,3 +96,5 @@
    11.4  val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*)
    11.5  case nxt of (Check_elementwise "Assumptions") => ()
    11.6  | _ => error "Check_elementwise changed; after switch sub-->root-method";
    11.7 +
    11.8 +(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)

    12.1 --- a/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml	Tue Aug 16 14:47:05 2022 +0200
    12.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml	Tue Aug 16 15:53:20 2022 +0200
    12.3 @@ -140,3 +140,5 @@
    12.4   = "([\"\n(e_e, - 1 + x = 0)\", \"\n(v_v, x)\", \"\n(L_L, [x = 1])\"], [R, R, D], empty, NONE, \n[x = 1],"^
    12.5    " ORundef, true, false)"
    12.6  then () else error "";
    12.7 +
    12.8 +(*ctxt* )Proof_Context.theory_of (Ctree.get_ctxt pt p);( *ctxt CANNOT BE RETRIEVED*)

    13.1 --- a/test/Tools/isac/Minisubpbl/600-postcond.sml	Tue Aug 16 14:47:05 2022 +0200
    13.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond.sml	Tue Aug 16 15:53:20 2022 +0200
    13.3 @@ -35,4 +35,7 @@
    13.4  if p = ([], Res)
    13.5  then case nxt of End_Proof' => ()
    13.6    | _ => error "calculation not finished correctly 1"
    13.7 -else error "calculation not finished correctly 2" 
    13.8 +else error "calculation not finished correctly 2";
    13.9 +
   13.10 +(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
   13.11 +

    14.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml	Tue Aug 16 14:47:05 2022 +0200
    14.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml	Tue Aug 16 15:53:20 2022 +0200
    14.3 @@ -171,3 +171,6 @@
    14.4    "4.   [x = 1]\n"
    14.5  (*".  [x = 1]"                           only shown by Test_Tool.show_pt*)
    14.6  then () else error "intermediate steps CHANGED";
    14.7 +
    14.8 +(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
    14.9 +

    15.1 --- a/test/Tools/isac/Minisubpbl/710-interSteps-short.sml	Tue Aug 16 14:47:05 2022 +0200
    15.2 +++ b/test/Tools/isac/Minisubpbl/710-interSteps-short.sml	Tue Aug 16 15:53:20 2022 +0200
    15.3 @@ -78,3 +78,5 @@
    15.4    "4.   [x = 1]\n"
    15.5  (*".  [x = 1]"                           only by Test_Tool.show_pt_tac*)
    15.6  then () else error "intermediate steps CHANGED";
    15.7 +
    15.8 +(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)

    16.1 --- a/test/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml	Tue Aug 16 14:47:05 2022 +0200
    16.2 +++ b/test/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml	Tue Aug 16 15:53:20 2022 +0200
    16.3 @@ -57,4 +57,7 @@
    16.4    case get_obj g_tac pt (fst p) of
    16.5      Apply_Method ["Test", "squ-equ-test-subpbl1"] => ()
    16.6    | _ => error "Minisubpbl/790-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 2"
    16.7 -else error "Minisubpbl/790-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 1"
    16.8 +else error "Minisubpbl/790-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 1";
    16.9 +
   16.10 +(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
   16.11 +

    17.1 --- a/test/Tools/isac/Minisubpbl/790-complete.sml	Tue Aug 16 14:47:05 2022 +0200
    17.2 +++ b/test/Tools/isac/Minisubpbl/790-complete.sml	Tue Aug 16 15:53:20 2022 +0200
    17.3 @@ -45,3 +45,5 @@
    17.4     "4.   [x = 1]\n"
    17.5  then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
    17.6  else error "re-build: fun locate_input_tactic changed";
    17.7 +
    17.8 +(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)

    18.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml	Tue Aug 16 14:47:05 2022 +0200
    18.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml	Tue Aug 16 15:53:20 2022 +0200
    18.3 @@ -190,3 +190,6 @@
    18.4  ([1], Res), 2 + - 1 + x = 2
    18.5  . . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]] 
    18.6  *)
    18.7 +
    18.8 +(*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
    18.9 +