1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Mon Aug 02 15:27:47 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Mon Aug 02 15:30:41 2021 +0200
     1.3 @@ -322,7 +322,6 @@
     1.4  
     1.5  (** )end;( *local*)
     1.6  
     1.7 -\<close> ML \<open>
     1.8  val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
     1.9  if ord_make_polynomial_in true @{theory} subs (t1, t2) then ()  else error "still GREATER?";
    1.10