1.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Sat Feb 04 16:49:08 2023 +0100
     1.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Sat Feb 04 17:00:25 2023 +0100
     1.3 @@ -51,13 +51,13 @@
     1.4  
     1.5  (*+*)val PblObj {ctxt, ...} = get_obj I pt [3];
     1.6  (*+isa==isa2*)ContextC.get_assumptions ctxt = [];
     1.7 -(*+isa==isa2*)(Ctree.get_assumptions pt p |> map (UnparseC.term_in_ctxt @{context})) = [];
     1.8 +(*+isa==isa2*)(Ctree.get_assumptions pt p |> map (UnparseC.term @{context})) = [];
     1.9  
    1.10          LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;
    1.11  "~~~~~ fun by_tactic , args:"; val (Tactic.Apply_Method' (mI, _, _, _), (_, ctxt), (pt, (pos as (p, _))))
    1.12    = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), (pt, p));
    1.13  
    1.14 -(*+isa==isa2*)if (ContextC.get_assumptions ctxt |> map (UnparseC.term_in_ctxt ctxt))
    1.15 +(*+isa==isa2*)if (ContextC.get_assumptions ctxt |> map (UnparseC.term ctxt))
    1.16  (*+*)   = ["precond_rootmet x"]
    1.17  (*+*)then () else error "assumptions 7 from Apply_Method'";
    1.18  
    1.19 @@ -66,7 +66,7 @@
    1.20             PblObj {meth = itms, origin = (oris, _, _), probl(*, ctxt*), ...} => (itms, oris, probl(*, ctxt*))
    1.21           | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj";
    1.22  
    1.23 -(*+isa==isa2*)if (ContextC.get_assumptions ctxt |> map (UnparseC.term_in_ctxt ctxt))
    1.24 +(*+isa==isa2*)if (ContextC.get_assumptions ctxt |> map (UnparseC.term ctxt))
    1.25  (*+*)   = ["precond_rootmet x"]
    1.26  (*+*)then () else error "assumptions 8";
    1.27  
    1.28 @@ -77,7 +77,7 @@
    1.29             (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
    1.30           | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate";
    1.31  
    1.32 -(*+*)(ContextC.get_assumptions ctxt |> map (UnparseC.term_in_ctxt ctxt))
    1.33 +(*+*)(ContextC.get_assumptions ctxt |> map (UnparseC.term ctxt))
    1.34  (*+isa==isa2*)  = ["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"]; 
    1.35  
    1.36          val ini = LItool.implicit_take ctxt prog env;
    1.37 @@ -87,7 +87,7 @@
    1.38            val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
    1.39            val (pos, c, _, pt) = Solve_Step.add show_add (is, ctxt) (pt, pos);
    1.40  
    1.41 -(*+*)if (ContextC.get_assumptions ctxt |> map (UnparseC.term_in_ctxt ctxt))
    1.42 +(*+*)if (ContextC.get_assumptions ctxt |> map (UnparseC.term ctxt))
    1.43  (*+isa==isa2*) = ["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"]
    1.44  (*+*)then () else error "assumptions 9";
    1.45  
    1.46 @@ -196,7 +196,7 @@
    1.47  then () else error "Minisubpbl/400-start-meth-subpbl changed";
    1.48  
    1.49  (*+*)val p_frm = ([3], Frm);
    1.50 -(*+*)if (Ctree.get_assumptions pt p_frm |> map (UnparseC.term_in_ctxt @{context}))
    1.51 +(*+*)if (Ctree.get_assumptions pt p_frm |> map (UnparseC.term @{context}))
    1.52  (*+*)   = ["precond_rootmet x"]
    1.53  (*+*)then () else error "p_frm BEFORE Apply_Method at Subproblem CHANGED";
    1.54  
    1.55 @@ -206,11 +206,11 @@
    1.56  (*+*)then () else error "assumptions<>[] before Apply_Method of Subproblem";
    1.57  
    1.58  (*+*)val ([3, 1], Frm) = p'''';
    1.59 -(*+*)if (Ctree.get_assumptions pt p'''' |> map (UnparseC.term_in_ctxt @{context}))
    1.60 +(*+*)if (Ctree.get_assumptions pt p'''' |> map (UnparseC.term @{context}))
    1.61  (*+*)   = ["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"]
    1.62  (*+*)then () else error "FALSE: 2 assumptions recorded Apply_Method of Subproblem";
    1.63  
    1.64  (*+*)val p_res = ([3], Res);
    1.65 -(*+*)if (Ctree.get_assumptions pt p_res |> map (UnparseC.term_in_ctxt @{context}))
    1.66 +(*+*)if (Ctree.get_assumptions pt p_res |> map (UnparseC.term @{context}))
    1.67  (*+*)   = ["precond_rootmet x"]
    1.68  (*+*)then () else error "p_res AFTER Apply_Method at Subproblem CHANGED";