--- 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 =