1.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml	Tue May 24 16:47:31 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml	Thu May 26 12:44:51 2022 +0200
     1.3 @@ -94,10 +94,10 @@
     1.4  if UnparseC.term t' = "True" then () 
     1.5  else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
     1.6  
     1.7 -val SOME t = TermC.parse thy "solution LL";
     1.8 -TermC.atomty (Thm.term_of t);
     1.9 -val SOME t = TermC.parse thy "solution LL";
    1.10 -TermC.atomty (Thm.term_of t);
    1.11 +val SOME t = TermC.parseNEW ctxt "solution LL";
    1.12 +TermC.atomty t;
    1.13 +val SOME t = TermC.parseNEW ctxt "solution LL";
    1.14 +TermC.atomty t;
    1.15  
    1.16  val t = TermC.str2term 
    1.17  "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";