1.1 --- a/test/Tools/isac/Interpret/rewtools.sml	Tue Apr 14 15:56:15 2020 +0200
     1.2 +++ b/test/Tools/isac/Interpret/rewtools.sml	Wed Apr 15 10:07:43 2020 +0200
     1.3 @@ -139,7 +139,7 @@
     1.4              val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
     1.5              val thm_deriv = Thm.get_name_hint thm;
     1.6  
     1.7 -if thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv)
     1.8 +if thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv)
     1.9     = "thy_isac_Test-thm-radd_left_commute" then ()
    1.10  else error "context_thy mini-subpbl ([2,4], Res) changed";
    1.11  (*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-radd_left_commute*
    1.12 @@ -161,7 +161,7 @@
    1.13    applicable_in pos pt tac
    1.14               val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
    1.15               val thm_deriv = Thm.get_name_hint thm;
    1.16 -if thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv) =
    1.17 +if thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv) =
    1.18    "thy_isac_Test-thm-risolate_bdv_add" then ()
    1.19  else error "context_thy mini-subpbl ([3,1,1], Frm) changed";
    1.20  (*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-risolate_bdv_add*