src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML

           handle exn =>
             if Exn.is_interrupt exn orelse debug then
               reraise exn
             else
               {outcome = SOME (SMT2_Failure.Other_Failure (Runtime.exn_message exn)),
-               rewrite_rules = [], conjecture_id = ~1, helper_ids = [], fact_ids = [],
-               z3_proof = []}
+               rewrite_rules = [], conjecture_id = ~1, prem_ids = [], helper_ids = [],
+               fact_ids = [], z3_proof = []}
 
         val death = Timer.checkRealTimer timer
         val outcome0 = if is_none outcome0 then SOME outcome else outcome0
         val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
         val timeout = Time.- (timeout, Timer.checkRealTimer timer)

       let val num_facts = length facts in
         map (weight_smt2_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1))
       end
 
     val weighted_factss = map (apsnd weight_facts) factss
-    val {outcome, filter_result = {conjecture_id, rewrite_rules, helper_ids, fact_ids, z3_proof,
-           ...}, used_from, run_time} =
+    val {outcome, filter_result = {rewrite_rules, conjecture_id, prem_ids, helper_ids, fact_ids,
+           z3_proof, ...}, used_from, run_time} =
       smt2_filter_loop name params state goal subgoal weighted_factss
     val used_named_facts = map snd fact_ids
     val used_facts = map fst used_named_facts
     val outcome = Option.map failure_of_smt2_failure outcome
 

          fn preplay =>
             let
               val fact_ids =
                 map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
                 map (fn (id, ((name, _), _)) => (id, name)) fact_ids
-              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy rewrite_rules conjecture_id
+              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy rewrite_rules prem_ids conjecture_id
                 fact_ids z3_proof
               val isar_params =
                 K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
                    minimize <> SOME false, atp_proof, goal)
               val one_line_params =