diff -r 798e54862b08 -r a25716353782 test/Tools/isac/Interpret/error-pattern.sml
--- a/test/Tools/isac/Interpret/error-pattern.sml	Thu Dec 08 10:33:27 2022 +0100
+++ b/test/Tools/isac/Interpret/error-pattern.sml	Thu Dec 08 17:55:45 2022 +0100
@@ -120,17 +120,17 @@
 		       ((#rules o Rule_Set.rep) Test_simplify)
 		       (sqrt_right false) NONE 
 		       (TermC.parse_test @{context} "x + 1 + - 1 * 2 = 0");
- (writeln o Derive.trtas2str) fod;
+ (writeln o (Derive.trtas2str ctxt)) fod;
 
  val ifod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls 
 		       ((#rules o Rule_Set.rep) Test_simplify)
 		       (sqrt_right false) NONE 
 		       (TermC.parse_test @{context} "- 2 * 1 + (1 + x) = 0");
- (writeln o Derive.trtas2str) ifod;
+ (writeln o (Derive.trtas2str ctxt)) ifod;
  fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;
  val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
  val der = fod' @ (map Derive.rev_deriv' rifod');
- (writeln o Derive.trtas2str) der;
+ (writeln o (Derive.trtas2str ctxt)) der;
  "----------------------------------------------------------";
 DEconstrCalcTree 1;
 
@@ -1096,7 +1096,7 @@
       {errpats, program = Rule.Prog prog, ...} => (errpats, prog)
     | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt"
     val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
-    val subst = Subst.for_bdv prog env
+    val subst = Subst.for_bdv ctxt prog env
     val errpatthms = errpats
       |> filter ((curry op = errpatID) o (#1: Error_Pattern.T -> Error_Pattern.id))
       |> map (#3: Error_Pattern.T -> thm list)