# HG changeset patch
# User blanchet
# Date 1643733192 -3600
# Node ID 79b4e711d6a296e3cfa21d420cc08b94f7a92417
# Parent  04a4881ff0fd66266980d139b5d111aae9dffbbd
robustly handle empty proof blocks in Isar proof output

diff -r 04a4881ff0fd -r 79b4e711d6a2 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 01 17:11:26 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 01 17:33:12 2022 +0100
@@ -254,8 +254,8 @@
               exists (is_referenced_in_step l) steps
 
             fun insert_lemma_in_step lem
-                  (step as Prove {qualifiers, obtains, label, goal, subproofs, facts = (ls, gs),
-                  proof_methods, comment}) =
+                (step as Prove {qualifiers, obtains, label, goal, subproofs, facts = (ls, gs),
+                 proof_methods, comment}) =
               let val l' = the (label_of_isar_step lem) in
                 if member (op =) ls l' then
                   [lem, step]
@@ -352,7 +352,7 @@
                   if is_clause_tainted c then
                     (case gamma of
                       [g] =>
-                      if skolem andalso is_clause_tainted g then
+                      if skolem andalso is_clause_tainted g andalso not (null accum) then
                         let
                           val skos = skolems_of ctxt (prop_of_clause g)
                           val subproof = Proof {fixes = skos, assumptions = [], steps = rev accum}
@@ -466,7 +466,7 @@
                 (if is_less (play_outcome_ord (play_outcome, one_line_play)) then
                    (case isar_proof of
                      Proof {steps = [Prove {facts = (_, gfs), proof_methods = meth :: _, ...}],
-                     ...} =>
+                       ...} =>
                      let
                        val used_facts' =
                          map_filter (fn s =>
diff -r 04a4881ff0fd -r 79b4e711d6a2 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Tue Feb 01 17:11:26 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Tue Feb 01 17:33:12 2022 +0100
@@ -352,7 +352,7 @@
         val assumptions' = map (apsnd (subst_atomic subst')) assumptions
         val steps' = fst (fold_map rationalize_step steps subst_ctxt')
       in
-        Proof { fixes = fixes', assumptions = assumptions', steps = steps'}
+        Proof {fixes = fixes', assumptions = assumptions', steps = steps'}
       end
   in
     rationalize_proof true ([], ctxt)
@@ -441,7 +441,7 @@
         val suffix = " }"
       in
         replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
-        String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^
+        String.substring (s, ind * indent_size, size s - ind * indent_size - 1) ^
         suffix ^ "\n"
       end
     and of_subproofs _ _ _ [] = ""
@@ -475,6 +475,7 @@
       |> fold (add_assm ind) assumptions
       |> add_steps ind steps
       |> fst
+      |> (fn s => if s = "" then of_indent ind ^ "\n" else s)  (* robustness *)
   in
     (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
     of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^