diff -r f1c6e778e412 -r e89709b80b6e src/HOL/Tools/SMT/verit_proof.ML
--- a/src/HOL/Tools/SMT/verit_proof.ML	Sat Mar 12 23:21:28 2022 +0100
+++ b/src/HOL/Tools/SMT/verit_proof.ML	Fri Mar 11 09:22:13 2022 +0100
@@ -483,13 +483,13 @@
   end
 
 fun normalized_rule_name id rule =
-  (case (rule = input_rule, can (unprefix SMTLIB_Interface.assert_prefix) id) of
+  (case (rule = input_rule, can SMTLIB_Interface.role_and_index_of_assert_name id) of
     (true, true) => normalized_input_rule
   | (true, _) => local_input_rule
   | _ => rule)
 
 fun is_assm_repetition id rule =
-  rule = input_rule andalso can (unprefix SMTLIB_Interface.assert_prefix) id
+  rule = input_rule andalso can SMTLIB_Interface.role_and_index_of_assert_name id
 
 fun extract_skolem ([SMTLIB.Sym var, typ, choice]) = (var, typ, choice)
   | extract_skolem t = raise Fail ("fail to parse type" ^ @{make_string} t)