--- 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 =>
--- 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 ^