1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Sat Aug 06 17:36:59 2022 +0200
     1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Sat Aug 06 18:00:33 2022 +0200
     1.3 @@ -329,7 +329,7 @@
     1.4  "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
     1.5  "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
     1.6  "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
     1.7 - reset_states ();
     1.8 + reset_states (); 
     1.9   CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], 
    1.10  	    ("Test", ["sqroot-test", "univariate", "equation", "test"],
    1.11  	     ["Test", "squ-equ-test-subpbl1"]))];
    1.12 @@ -1095,7 +1095,7 @@
    1.13        |> map (#3: Error_Pattern.T -> thm list)
    1.14        |> flat;
    1.15  
    1.16 -case map (Error_Pattern.fill_from_store subst f_curr errpatID) errpatthms |> flat of
    1.17 +case map (Error_Pattern.fill_from_store ctxt subst f_curr errpatID) errpatthms |> flat of
    1.18    ("fill-d_d-arg", tm, thm, subs_opt) :: _ => if UnparseC.term tm = 
    1.19      "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1"
    1.20      then () else error "find_fill_patterns changed 1a"
    1.21 @@ -1107,7 +1107,7 @@
    1.22          val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv
    1.23          val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
    1.24          val Thy_Write.Hthm {fillpats, ...} = Thy_Read.from_store theID
    1.25 -        val some = map (Error_Pattern.fill_form subst (thm, form) errpatID) fillpats;
    1.26 +        val some = map (Error_Pattern.fill_form ctxt subst (thm, form) errpatID) fillpats;
    1.27  
    1.28  case some |> filter is_some |> map the of
    1.29    ("fill-d_d-arg", tm, thm, subsopt) :: _ => if UnparseC.term tm = 
    1.30 @@ -1125,7 +1125,7 @@
    1.31  else error "find_fill_patterns changed 3";
    1.32  
    1.33  "~~~~~ to findFillpatterns return val:"; val (fillpats) =
    1.34 -  (map (Error_Pattern.fill_from_store (subs_opt, subst) f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*);
    1.35 +  (map (Error_Pattern.fill_from_store ctxt (subs_opt, subst) f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*);
    1.36  
    1.37  "vvv--- dropped this code WN120730";
    1.38  val msg = "fill patterns " ^