fixed generation of Isar proofs e89709b80b6e

--- a/src/HOL/Tools/SMT/cvc4_proof_parse.ML	Fri Mar 11 09:22:13 2022 +0100
+++ b/src/HOL/Tools/SMT/cvc4_proof_parse.ML	Mon Mar 28 17:16:42 2022 +0200
@@ -37,7 +37,7 @@
 
       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
     in

--- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Mar 11 09:22:13 2022 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Mon Mar 28 17:16:42 2022 +0200
@@ -32,7 +32,7 @@
     terms: term Symtab.table,
     ll_defs: term list,
     rewrite_rules: thm list,
-    assms: (int * thm) list }
+    assms: ((int * SMT_Util.role) * thm) list }
 
   (*translation*)
   val add_config: SMT_Util.class * (Proof.context -> config) -> Context.generic -> Context.generic
@@ -79,7 +79,7 @@
   terms: term Symtab.table,
   ll_defs: term list,
   rewrite_rules: thm list,
-  assms: (int * thm) list }
+  assms: ((int * SMT_Util.role) * thm) list }
 
 
 (* translation context *)
@@ -133,7 +133,7 @@
     val terms' = Termtab.fold add_fun terms Symtab.empty
   in
     {context = ctxt, typs = typs', terms = terms', ll_defs = ll_defs, rewrite_rules = rules,
-     assms = map (apfst fst) assms}
+     assms = assms}
   end
 
 

--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Mar 11 09:22:13 2022 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Mar 28 17:16:42 2022 +0200
@@ -148,8 +148,8 @@
 
 fun unprefix_axiom s =
   try (pair SMT_Util.Conjecture o unprefix conjecture_prefix) s
-  |> curry merge_options (try (pair SMT_Util.Conjecture o unprefix hypothesis_prefix) s)
-  |> curry merge_options (try (pair SMT_Util.Conjecture o unprefix axiom_prefix) s)
+  |> curry merge_options (try (pair SMT_Util.Hypothesis o unprefix hypothesis_prefix) s)
+  |> curry merge_options (try (pair SMT_Util.Axiom o unprefix axiom_prefix) s)
   |> the
 
 fun role_and_index_of_assert_name s =

--- a/src/HOL/Tools/SMT/verit_proof_parse.ML	Fri Mar 11 09:22:13 2022 +0100
+++ b/src/HOL/Tools/SMT/verit_proof_parse.ML	Mon Mar 28 17:16:42 2022 +0200
@@ -35,9 +35,9 @@
     val id_of_index = Integer.add num_ll_defs
     val index_of_id = Integer.add (~ num_ll_defs)
 
-    fun step_of_assume j (_, th) =
+    fun step_of_assume j ((_, role), th) =
       Verit_Proof.VeriT_Step
-        {id = SMTLIB_Interface.assert_name_of_role_and_index SMT_Util.Axiom (id_of_index j),
+        {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, _) = Verit_Proof.parse typs terms output ctxt
@@ -60,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' @

--- a/src/HOL/Tools/SMT/verit_replay.ML	Fri Mar 11 09:22:13 2022 +0100
+++ b/src/HOL/Tools/SMT/verit_replay.ML	Mon Mar 28 17:16:42 2022 +0200
@@ -272,7 +272,7 @@
     fun cond rule = rule = Verit_Proof.input_rule
     val add_asssert = SMT_Replay.add_asserted Symtab.update Symtab.empty extract cond
     val ((_, _), (ctxt3, assumed)) =
-      add_asssert outer_ctxt rewrite_rules assms
+      add_asssert outer_ctxt rewrite_rules (map (apfst fst) assms)
         (map_filter (remove_rewrite_rules_from_rules num_ll_defs) assm_steps) ctxt2
 
     val used_rew_js =

--- a/src/HOL/Tools/SMT/z3_replay.ML	Fri Mar 11 09:22:13 2022 +0100
+++ b/src/HOL/Tools/SMT/z3_replay.ML	Mon Mar 28 17:16:42 2022 +0200
@@ -123,7 +123,7 @@
     xfacts prems concl output =
   let
     val (steps, ctxt2) = Z3_Proof.parse typs terms output ctxt
-    val ((iidths, _), _) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2
+    val ((iidths, _), _) = add_asserted outer_ctxt rewrite_rules (map (apfst fst) assms) steps ctxt2
 
     fun id_of_index i = the_default ~1 (Option.map fst (AList.lookup (op =) iidths i))
 
@@ -153,7 +153,7 @@
   let
     val (steps, ctxt2) = Z3_Proof.parse typs terms output ctxt
     val ((_, rules), (ctxt3, assumed)) =
-      add_asserted outer_ctxt rewrite_rules assms steps ctxt2
+      add_asserted outer_ctxt rewrite_rules (map (apfst fst) assms) steps ctxt2
     val ctxt4 =
       ctxt3
       |> put_simpset (SMT_Replay.make_simpset ctxt3 [])