1.1 --- a/test/Tools/isac/Knowledge/rational-2.sml	Tue May 24 16:47:31 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml	Thu May 26 12:44:51 2022 +0200
     1.3 @@ -755,7 +755,7 @@
     1.4  if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))"
     1.5     andalso ThmC.string_of_thm thm = 
     1.6             (string_of_thm (Thm.make_thm @{theory "Isac_Knowledge"}
     1.7 -               (Trueprop $ (Thm.term_of o the o (TermC.parse thy)) "9 = 3 \<up> 2"))) then ()
     1.8 +               (Trueprop $ (TermC.parseNEW' ctxt "9 = 3 \<up> 2"))) then ()
     1.9  else error "rational.sml next_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";
    1.10  \---------------------------------------------------------------------------------------/*)
    1.11  
    1.12 @@ -774,7 +774,7 @@
    1.13    val SOME (r as (Thm (str, thm))) = nex revsets t;
    1.14  if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso
    1.15     ThmC.string_of_thm thm = (string_of_thm (ThmC_Def.make_thm @{theory "Isac_Knowledge"}
    1.16 -                (Trueprop $ (Thm.term_of o the o (TermC.parse thy)) "9 = 3 \<up> 2"))) then ()
    1.17 +                (Trueprop $ (TermC.parseNEW' ctxt "9 = 3 \<up> 2"))) then ()
    1.18  else error "rational.sml next_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";
    1.19  
    1.20  (*check the next rule*)
    1.21 @@ -1607,7 +1607,8 @@
    1.22  "-------- fun eval_get_denominator -------------------------------------------";
    1.23  "-------- fun eval_get_denominator -------------------------------------------";
    1.24  val thy = @{theory Isac_Knowledge};
    1.25 -val t = Thm.term_of (the (TermC.parse thy "get_denominator ((a +x)/b)"));
    1.26 +val ctxt = Proof_Context.init_global thy;
    1.27 +val t = TermC.parseNEW' ctxt "get_denominator ((a +x)/b)";
    1.28  val SOME (_, t') = eval_get_denominator "" 0 t thy;
    1.29  if UnparseC.term t' = "get_denominator ((a + x) / b) = b"
    1.30  then () else error "get_denominator ((a + x) / b) = b"