1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Sun Oct 23 16:08:27 2022 +0200
     1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Sun Oct 23 17:21:04 2022 +0200
     1.3 @@ -740,7 +740,7 @@
     1.4  (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
     1.5  autoCalculate 1 (Steps 1);
     1.6  val ((pt,p),_) = States.get_calc 1;
     1.7 -val Form res = (#1 o ME_Misc.pt_extract) (pt, p);
     1.8 +val Form res = (#1 o (ME_Misc.pt_extract ctxt)) (pt, p);
     1.9  if UnparseC.term res = "d_d x (x \<up> 2 + x + 1)" then ()
    1.10  else error "diff.sml Diff (x \<up> 2 + x + 1, x) from exp";
    1.11  DEconstrCalcTree 1;
    1.12 @@ -1173,7 +1173,7 @@
    1.13    instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
    1.14    val ((pt,pos), _) = States.get_calc 1;
    1.15    val p = States.get_pos 1 1;
    1.16 -  val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
    1.17 +  val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
    1.18  
    1.19    if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" then
    1.20      case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"], 
    1.21 @@ -1189,7 +1189,7 @@
    1.22    val ((pt,pos),_) = States.get_calc 1;
    1.23    val p = States.get_pos 1 1;
    1.24  
    1.25 -  val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
    1.26 +  val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
    1.27    if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" then
    1.28      case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"], 
    1.29        ("diff_sum", thm)) =>
    1.30 @@ -1202,7 +1202,7 @@
    1.31    (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
    1.32    val ((pt,pos),_) = States.get_calc 1;
    1.33    val p = States.get_pos 1 1;
    1.34 -  val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
    1.35 +  val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
    1.36    if p = ([1], Res) andalso existpt [2] pt
    1.37      andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
    1.38    then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"], 
    1.39 @@ -1241,7 +1241,7 @@
    1.40  "~~~~~ final check:";
    1.41  val ((pt, _),_) = States.get_calc 1;
    1.42  val p = States.get_pos 1 1;
    1.43 -val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
    1.44 +val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
    1.45    if p = ([2], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)"
    1.46    then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"], 
    1.47        ("diff_sin_chain", thm)) =>