1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Mon Apr 13 13:27:55 2020 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Mon Apr 13 15:31:23 2020 +0200
     1.3 @@ -140,7 +140,7 @@
     1.4  " _________________ rewrite_ x+4_________________ ";
     1.5  " _________________ rewrite_ x+4_________________ ";
     1.6  val t = (Thm.term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
     1.7 -val thm = num_str @{thm square_equation_left};
     1.8 +val thm = ThmC.numerals_to_Free @{thm square_equation_left};
     1.9  val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t);
    1.10  val rls = Test_simplify;
    1.11  val (t,_) = the (rewrite_set_ thy false rls t);
    1.12 @@ -184,7 +184,7 @@
    1.13  
    1.14  28.8.02: ruleset besser zusammenstellen !!!
    1.15  *)
    1.16 -val thm = num_str @{thm square_equation_left};
    1.17 +val thm = ThmC.numerals_to_Free @{thm square_equation_left};
    1.18  val (t,asm') = the (rewrite_ thy tless_true tval_rls true thm t);
    1.19  val asm = asm union asm';
    1.20  val rls = Test_simplify;
    1.21 @@ -206,7 +206,7 @@
    1.22  " _________________ rewrite x=4_________________ ";
    1.23  " _________________ rewrite x=4_________________ ";
    1.24  (*
    1.25 -rewrite thy' "tless_true" "tval_rls" true (num_str @{thm rbinom_power_2}) ct;
    1.26 +rewrite thy' "tless_true" "tval_rls" true (ThmC.numerals_to_Free @{thm rbinom_power_2}) ct;
    1.27  atomty ((#prop o Thm.rep_thm) (!tthm));
    1.28  atomty (Thm.term_of (!tct));
    1.29  *)