1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Sat Aug 06 15:57:46 2022 +0200
     1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Sat Aug 06 17:36:59 2022 +0200
     1.3 @@ -284,7 +284,7 @@
     1.4  2.5.   1 + (x + -2 * 1) = 0\n
     1.5  2.6.   1 + x + -2 * 1 = 0\n";
     1.6  *)
     1.7 -if str = 
     1.8 +if str =
     1.9  ".    ----- pblobj -----\n"^
    1.10  "1.   x + 1 = 2\n"^
    1.11  "2.   x + 1 + - 1 * 2 = 0\n"^
    1.12 @@ -925,21 +925,21 @@
    1.13  
    1.14  val pat = TermC.parse_patt @{theory} "(?a + ?b)/?a = ?b";
    1.15  val (res, inf) = (TermC.str2term "(2 + 3)/2", TermC.str2term "3");
    1.16 -if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    1.17 +if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    1.18  then () else error "error patt example1 changed";
    1.19  
    1.20  val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";
    1.21  val (res, inf) = (TermC.str2term "(2 + 3)/(2 + 4)", TermC.str2term "3 / 4");
    1.22 -if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    1.23 +if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    1.24  then () else error "error patt example2 changed";
    1.25  
    1.26  val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
    1.27  val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "2 / 4");
    1.28 -if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    1.29 +if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    1.30  then () else error "error patt example3 changed";
    1.31  
    1.32  val inf =  TermC.str2term "1 / 2";
    1.33 -if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    1.34 +if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    1.35  then () else error "error patt example3 changed";
    1.36  
    1.37  "--------- build fun check_for' ?bdv -------------------------";
    1.38 @@ -977,7 +977,7 @@
    1.39  if norm_res = norm_inf then ()
    1.40  else error "build fun check_for' ?bdv changed 5";
    1.41  
    1.42 -if Error_Pattern.check_for' (res, inf) (subst: subst) ("errpatID": Error_Pattern.id, pat) rls = SOME "errpatID"
    1.43 +if Error_Pattern.check_for' ctxt (res, inf) (subst: subst) ("errpatID": Error_Pattern.id, pat) rls = SOME "errpatID"
    1.44  then () else error "error patt example1 changed";
    1.45  
    1.46  "--------- build fun check_for ------------------------";
    1.47 @@ -999,7 +999,7 @@
    1.48        TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
    1.49       [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, 
    1.50        @{thm diff_ln_chain}, @{thm  diff_exp_chain}])];
    1.51 -case Error_Pattern.check_for (res, inf) (prog, env) (errpats, rls) of SOME _ => () 
    1.52 +case Error_Pattern.check_for ctxt (res, inf) (prog, env) (errpats, rls) of SOME _ => () 
    1.53  | NONE => error "Error_Pattern.check_for broken";
    1.54  DEconstrCalcTree 1;
    1.55  
    1.56 @@ -1053,7 +1053,7 @@
    1.57  (*+*)   UnparseC.term f_in = "d_d x (x \<up> 2) + cos (4 * x \<up> 3)"
    1.58  (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 2";
    1.59  
    1.60 -             val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) (*of*);
    1.61 +             val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.check_for ctxt (f_pred, f_in) (prog, env) (errpats, nrls) (*of*);
    1.62  
    1.63  "--- final check:";
    1.64  (*+*)val (_, _, ptp') = cs';