1.1 --- a/test/Tools/isac/MathEngBasic/thmC.sml	Mon Jul 19 17:29:35 2021 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/thmC.sml	Mon Jul 19 18:29:46 2021 +0200
     1.3 @@ -63,7 +63,7 @@
     1.4  then () else error "fun revert_sym_rule changed 1";
     1.5  
     1.6  val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
     1.7 -  (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
     1.8 +  (Thm ("real_diff_minus", @{thm real_diff_minus}))
     1.9  ;
    1.10  if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + - 1 * ?b"
    1.11  then () else error "fun revert_sym_rule changed 2"