parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition

--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Sep 25 17:16:32 2023 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Sep 25 17:16:32 2023 +0200
@@ -514,8 +514,9 @@
    || $$ "(" |-- parse_hol_typed_var --| $$ ")") x
 
 fun parse_simple_hol_term x =
-  (parse_fol_quantifier -- ($$ "[" |-- parse_hol_typed_var --| $$ "]" --| $$ ":") -- parse_hol_term
-      >> (fn ((q, ys), t) =>
+  (parse_fol_quantifier -- ($$ "[" |-- parse_hol_typed_var --| $$ "]" --| $$ ":")
+      -- parse_simple_hol_term
+    >> (fn ((q, ys), t) =>
           fold_rev
             (fn (var, ty) => fn r =>
                 AAbs (((var, the_default dummy_atype ty), r), [])
@@ -632,7 +633,7 @@
 val parse_spass_annotations =
   Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name --| Scan.option ($$ ","))) []
 
-(* We ignore the stars and the pluses that follow literals. *)
+(* We ignore the stars and the pluses that follow literals in SPASS's output. *)
 fun parse_decorated_atom x =
   (parse_fol_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x
 

--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Sep 25 17:16:32 2023 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Sep 25 17:16:32 2023 +0200
@@ -271,12 +271,16 @@
 
     fun do_term opt_T u =
       (case u of
-        AAbs (((var, ty), term), []) =>
+        AAbs (((var, ty), term), us) =>
         let
           val typ = typ_of_atp_type ctxt ty
           val var_name = repair_var_name var
           val tm = do_term NONE term
-        in quantify_over_var true lambda' var_name typ tm end
+          val lam = quantify_over_var true lambda' var_name typ tm
+          val args = map (do_term NONE) us
+        in
+          list_comb (lam, args)
+        end
       | ATerm ((s, tys), us) =>
         if s = "" (* special marker generated on parse error *) then
           error "Isar proof reconstruction failed because the ATP proof contains unparsable \

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Sep 25 17:16:32 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Sep 25 17:16:32 2023 +0200
@@ -261,6 +261,8 @@
             and is_referenced_in_proof l (Proof {steps, ...}) =
               exists (is_referenced_in_step l) steps
 
+            (* We try to introduce pure lemmas (not "obtains") close to where
+               they are used. *)
             fun insert_lemma_in_step lem
                 (step as Prove {qualifiers, obtains, label, goal, subproofs, facts = (ls, gs),
                  proof_methods, comment}) =
@@ -286,7 +288,8 @@
               end
             and insert_lemma_in_steps lem [] = [lem]
               | insert_lemma_in_steps lem (step :: steps) =
-                if is_referenced_in_step (the (label_of_isar_step lem)) step then
+                if not (null (obtains_of_isar_step lem))
+                   orelse is_referenced_in_step (the (label_of_isar_step lem)) step then
                   insert_lemma_in_step lem step @ steps
                 else
                   step :: insert_lemma_in_steps lem steps

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Sep 25 17:16:32 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Sep 25 17:16:32 2023 +0200
@@ -46,6 +46,7 @@
   val steps_of_isar_proof : isar_proof -> isar_step list
   val isar_proof_with_steps : isar_proof -> isar_step list -> isar_proof
 
+  val obtains_of_isar_step : isar_step -> (string * typ) list
   val label_of_isar_step : isar_step -> label option
   val facts_of_isar_step : isar_step -> facts
   val proof_methods_of_isar_step : isar_step -> proof_method list
@@ -130,6 +131,9 @@
 fun isar_proof_with_steps (Proof {fixes, assumptions, ...}) steps =
   Proof {fixes = fixes, assumptions = assumptions, steps = steps}
 
+fun obtains_of_isar_step (Prove {obtains, ...}) = obtains
+  | obtains_of_isar_step _ = []
+
 fun label_of_isar_step (Prove {label, ...}) = SOME label
   | label_of_isar_step _ = NONE