1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Sat Apr 17 20:44:57 2021 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Sat Apr 17 21:10:27 2021 +0200
     1.3 @@ -200,7 +200,7 @@
     1.4  " _________________ rewrite x=4_________________ ";
     1.5  (*
     1.6  rewrite thy' "tless_true" "tval_rls" true (ThmC.numerals_to_Free @{thm rbinom_power_2}) ct;
     1.7 -atomty ((#prop o Thm.rep_thm) (!tthm));
     1.8 +atomty (Thm.prop_of (!tthm));
     1.9  atomty (Thm.term_of (!tct));
    1.10  *)
    1.11  val thy' = "Test";