test/Tools/isac/Interpret/error-pattern.sml
changeset 60681 dcc82831573a
parent 60676 8c37f1009457
child 60766 2e0603ca18a4
     1.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Wed Feb 08 07:51:39 2023 +0100
     1.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Wed Feb 08 08:59:37 2023 +0100
     1.3 @@ -1139,9 +1139,9 @@
     1.4      val thm_id_long = Thm.get_name_hint thm
     1.5  
     1.6  (*+*)val "Diff.diff_sin_chain" = thm_id_long;
     1.7 -(*+*)val "diff_sin_chain" = ThmC.cut_id thm_id_long;
     1.8 +(*+*)val "diff_sin_chain" = ThmC.cut_longid thm_id_long;
     1.9  
    1.10 -    val thm_id = ThmC.cut_id thm_id_long
    1.11 +    val thm_id = ThmC.cut_longid thm_id_long
    1.12      val fill_ins =
    1.13  
    1.14  Error_Pattern.get_fill_ins (Proof_Context.theory_of ctxt) thm_id;