src/HOL/Tools/ATP/atp_proof_reconstruct.ML

          singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
     isa_short_ext
   else
     isa_ext
 
-fun add_all_defs fact_names accum =
+fun add_non_rec_defs fact_names accum =
   Vector.foldl
       (fn (facts, facts') =>
-          union (op =) (filter (fn (_, (_, status)) => status = Def) facts)
+          union (op =)
+                (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts)
                 facts')
       accum fact_names
 
 fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, rule, deps)) =
     (if rule = leo2_ext then
        insert (op =) (ext_name ctxt, (Global, General))
      else if rule = leo2_unfold_def then
        (* LEO 1.3.3 does not record definitions properly, leading to missing
          dependencies in the TSTP proof. Remove the next line once this is
          fixed. *)
-       add_all_defs fact_names
+       add_non_rec_defs fact_names
      else if rule = satallax_unsat_coreN then
        (fn [] =>
            (* Satallax doesn't include definitions in its unsatisfiable cores,
               so we assume the worst and include them all here. *)
-           [(ext_name ctxt, (Global, General))] |> add_all_defs fact_names
+           [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
          | facts => facts)
      else
        I)
     #> (if null deps then union (op =) (resolve_fact fact_names ss)
         else I)