1.1 --- a/test/Tools/isac/MathEngBasic/thmC.sml	Fri May 07 18:12:51 2021 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/thmC.sml	Tue Jun 01 15:41:23 2021 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4    (@{theory Isac_Knowledge},
     1.5      Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})));
     1.6  
     1.7 -if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm thm = "- ?z1 = -1 * ?z1" then ()
     1.8 +if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm thm = "- ?z1 = - 1 * ?z1" then ()
     1.9  else error "input to revert_sym_rule CHANGED";
    1.10  
    1.11        (*if*) is_sym (cut_id id) (*then*);
    1.12 @@ -61,11 +61,11 @@
    1.13  val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
    1.14    (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))
    1.15  ;
    1.16 -if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "-1 * ?z = - ?z"
    1.17 +if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "- 1 * ?z = - ?z"
    1.18  then () else error "fun revert_sym_rule changed 1";
    1.19  
    1.20  val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
    1.21    (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
    1.22  ;
    1.23 -if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + -1 * ?b"
    1.24 +if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + - 1 * ?b"
    1.25  then () else error "fun revert_sym_rule changed 2"