--- a/src/HOL/Tools/SMT/verit_isar.ML	Sat Mar 12 23:21:28 2022 +0100
+++ b/src/HOL/Tools/SMT/verit_isar.ML	Fri Mar 11 09:22:13 2022 +0100
@@ -34,7 +34,7 @@
       in
         if rule = input_rule then
           let
-            val id_num = the (Int.fromString (unprefix assert_prefix id))
+            val id_num = snd (SMTLIB_Interface.role_and_index_of_assert_name id)
             val ss = the_list (AList.lookup (op =) fact_helper_ids id_num)
           in
             (case distinguish_conjecture_and_hypothesis ss id_num conjecture_id prem_ids