post-merged into new Lethe code

--- a/src/HOL/Tools/SMT/lethe_proof_parse.ML	Tue Mar 29 12:55:25 2022 +0200
+++ b/src/HOL/Tools/SMT/lethe_proof_parse.ML	Tue Mar 29 13:31:45 2022 +0200
@@ -32,13 +32,16 @@
     val id_of_index = Integer.add num_ll_defs
     val index_of_id = Integer.add (~ num_ll_defs)
 
-    fun step_of_assume j (_, th) =
-      Lethe_Proof.Lethe_Step {id = SMTLIB_Interface.assert_name_of_role_and_index SMT_Util.Axiom (id_of_index j),
+    fun step_of_assume j ((_, role), th) =
+      Lethe_Proof.Lethe_Step
+        {id = SMTLIB_Interface.assert_name_of_role_and_index role (id_of_index j),
         rule = input_rule, prems = [], proof_ctxt = [], concl = Thm.prop_of th, fixes = []}
 
     val (actual_steps, _) = Lethe_Proof.parse typs terms output ctxt
     val used_assert_ids =
-        map_filter (try (snd o SMTLIB_Interface.role_and_index_of_assert_name)) output
+        actual_steps
+        |> map_filter (fn (Lethe_Step { id, ...}) =>
+           try (snd o SMTLIB_Interface.role_and_index_of_assert_name) id)
     val used_assm_js =
       map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end)
         used_assert_ids
@@ -57,10 +60,11 @@
     val prem_ids = map id_of_index (prems_i upto prems_i + num_prems - 1)
     val fact_ids' =
       map_filter (fn j =>
-        let val (i, _) = nth assms j in
+        let val ((i, _), _) = nth assms j in
           try (apsnd (nth xfacts)) (id_of_index j, i - facts_i)
         end) used_assm_js
-    val helper_ids' = filter (fn (i, _) => i >= helpers_i) used_assms
+    val helper_ids' =
+      map_filter (fn ((i, _), thm) => if i >= helpers_i then SOME (i, thm) else NONE) used_assms
 
     val fact_helper_ts =
       map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, Thm.prop_of th)) helper_ids' @