# HG changeset patch
# User blanchet
# Date 1701867918 -3600
# Node ID 2eb3dcae97819da1ac9800b09c555b0200d8200c
# Parent  4a4db49e6d0517bada76ca632634d08c0567758f
check that Isar proofs contain one 'show'

diff -r 4a4db49e6d05 -r 2eb3dcae9781 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Dec 06 12:45:57 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Dec 06 14:05:18 2023 +0100
@@ -477,8 +477,8 @@
               one_line_proof_text ctxt 0
                 (if is_less (play_outcome_ord (play_outcome, one_line_play)) then
                    (case isar_proof of
-                     Proof {steps = [Prove {facts = (_, gfs), proof_methods = meth :: _, ...}],
-                       ...} =>
+                     Proof {steps = [Prove {qualifiers = [Show], facts = (_, gfs),
+                       proof_methods = meth :: _, ...}], ...} =>
                      let
                        val used_facts' =
                          map_filter (fn s =>
@@ -489,7 +489,8 @@
                               SOME (s, (Global, General))) gfs
                      in
                        ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count)
-                     end)
+                     end
+                   | _ => one_line_params)
                  else
                    one_line_params) ^
               (if isar_proofs = SOME true then "\n(No Isar proof available)" else "")