1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Mon Jun 21 14:39:52 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Mon Jun 21 15:36:09 2021 +0200
     1.3 @@ -944,7 +944,7 @@
     1.4   val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
     1.5   val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
     1.6   val t' = UnparseC.term t;
     1.7 - (*if t'= "HOL.True" then ()
     1.8 + (*if t'= \<^const_name>\<open>True\<close> then ()
     1.9   else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
    1.10  (* *)
    1.11   val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)",