1.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Tue Apr 14 12:39:26 2020 +0200
     1.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Tue Apr 14 15:56:15 2020 +0200
     1.3 @@ -175,13 +175,13 @@
     1.4  val (Thm (thmID, thm)) = ThmC.revert_sym thy
     1.5    (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))
     1.6  ;
     1.7 -if thmID = "Poly.real_mult_minus1" andalso string_of_thmI thm = "-1 * ?z = - ?z"
     1.8 +if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "-1 * ?z = - ?z"
     1.9  then () else error "fun revert_sym changed 1";
    1.10  
    1.11  val (Thm (thmID, thm)) = ThmC.revert_sym thy
    1.12    (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
    1.13  ;
    1.14 -if thmID = "Root.real_diff_minus" andalso string_of_thmI thm = "?a - ?b = ?a + -1 * ?b"
    1.15 +if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + -1 * ?b"
    1.16  then () else error "fun revert_sym changed 2"
    1.17  
    1.18  "----------- fun thms_of_rlss ------------------------------------";