1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Thu Dec 08 10:33:27 2022 +0100
     1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Thu Dec 08 17:55:45 2022 +0100
     1.3 @@ -120,17 +120,17 @@
     1.4  		       ((#rules o Rule_Set.rep) Test_simplify)
     1.5  		       (sqrt_right false) NONE 
     1.6  		       (TermC.parse_test @{context} "x + 1 + - 1 * 2 = 0");
     1.7 - (writeln o Derive.trtas2str) fod;
     1.8 + (writeln o (Derive.trtas2str ctxt)) fod;
     1.9  
    1.10   val ifod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls 
    1.11  		       ((#rules o Rule_Set.rep) Test_simplify)
    1.12  		       (sqrt_right false) NONE 
    1.13  		       (TermC.parse_test @{context} "- 2 * 1 + (1 + x) = 0");
    1.14 - (writeln o Derive.trtas2str) ifod;
    1.15 + (writeln o (Derive.trtas2str ctxt)) ifod;
    1.16   fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;
    1.17   val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
    1.18   val der = fod' @ (map Derive.rev_deriv' rifod');
    1.19 - (writeln o Derive.trtas2str) der;
    1.20 + (writeln o (Derive.trtas2str ctxt)) der;
    1.21   "----------------------------------------------------------";
    1.22  DEconstrCalcTree 1;
    1.23  
    1.24 @@ -1096,7 +1096,7 @@
    1.25        {errpats, program = Rule.Prog prog, ...} => (errpats, prog)
    1.26      | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt"
    1.27      val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
    1.28 -    val subst = Subst.for_bdv prog env
    1.29 +    val subst = Subst.for_bdv ctxt prog env
    1.30      val errpatthms = errpats
    1.31        |> filter ((curry op = errpatID) o (#1: Error_Pattern.T -> Error_Pattern.id))
    1.32        |> map (#3: Error_Pattern.T -> thm list)