1.1 --- a/test/Tools/isac/Knowledge/rational-2.sml Tue Jul 20 14:37:56 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml Tue Jul 27 11:21:14 2021 +0200
1.3 @@ -784,7 +784,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 $ TermC.parseNEW'' thy "9 = 3 \<up> 2"))) then ()
1.8 + (Trueprop $ (Thm.term_of o the o (TermC.parse thy)) "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 @@ -803,7 +803,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 $ TermC.parseNEW'' thy "9 = 3 \<up> 2"))) then ()
1.17 + (Trueprop $ (Thm.term_of o the o (TermC.parse thy)) "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*)