test/Tools/isac/Interpret/error-pattern.sml
changeset 60424 c3acf9c442ac
parent 60360 49680d595342
child 60428 203438ff792f
     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*)