1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Tue May 24 16:47:31 2022 +0200
1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Thu May 26 12:44:51 2022 +0200
1.3 @@ -1026,8 +1026,7 @@
1.4 "~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Calc.state_post), istr)
1.5 = (cs', (encode ifo));
1.6 val ctxt = get_ctxt pt pos (*see TODO.thy*)
1.7 - val SOME f_in = (*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
1.8 - val f_in = Thm.term_of f_in
1.9 + val SOME f_in = (*case*) TermC.parseNEW ctxt istr (*of*);
1.10 val pos_pred = lev_back' pos
1.11 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
1.12 (*if*) f_pred = f_in; (*else*)