diff -r e728d3a3d383 -r 4ea19e5dc67e src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Oct 21 17:46:51 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Oct 22 15:18:08 2020 +0200
@@ -198,16 +198,24 @@
                 atp_proof
             val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof
 
-            fun add_lemma ((l, t), rule) ctxt =
+            fun add_lemma ((label, goal), rule) ctxt =
               let
-                val (skos, meths) =
-                  (if is_skolemize_rule rule then (skolems_of ctxt t, skolem_methods)
+                val (skos, proof_methods) =
+                  (if is_skolemize_rule rule then (skolems_of ctxt goal, skolem_methods)
                    else if is_arith_rule rule then ([], arith_methods)
                    else ([], rewrite_methods))
                   ||> massage_methods
+                val prove = Prove {
+                  qualifiers = [],
+                  obtains = skos,
+                  label = label,
+                  goal = goal,
+                  subproofs = [],
+                  facts = ([], []),
+                  proof_methods = proof_methods,
+                  comment = ""}
               in
-                (Prove ([], skos, l, t, [], ([], []), meths, ""),
-                 ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd))
+                (prove, ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd))
               end
 
             val (lems, _) =
@@ -239,25 +247,30 @@
                 atp_proof
 
             fun is_referenced_in_step _ (Let _) = false
-              | is_referenced_in_step l (Prove (_, _, _, _, subs, (ls, _), _, _)) =
-                member (op =) ls l orelse exists (is_referenced_in_proof l) subs
+              | is_referenced_in_step l (Prove {subproofs, facts = (ls, _), ...}) =
+                member (op =) ls l orelse exists (is_referenced_in_proof l) subproofs
             and is_referenced_in_proof l (Proof {steps, ...}) =
               exists (is_referenced_in_step l) steps
 
             fun insert_lemma_in_step lem
-                (step as Prove (qs, fix, l, t, subs, (ls, gs), meths, 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]
                 else
-                  let val refs = map (is_referenced_in_proof l') subs in
+                  let val refs = map (is_referenced_in_proof l') subproofs in
                     if length (filter I refs) = 1 then
-                      let
-                        val subs' = map2 (fn false => I | true => insert_lemma_in_proof lem) refs
-                          subs
-                      in
-                        [Prove (qs, fix, l, t, subs', (ls, gs), meths, comment)]
-                      end
+                      [Prove {
+                        qualifiers = qualifiers,
+                        obtains = obtains,
+                        label = label,
+                        goal = goal,
+                        subproofs =
+                          map2 (fn false => I | true => insert_lemma_in_proof lem) refs subproofs,
+                        facts = (ls, gs),
+                        proof_methods = proof_methods,
+                        comment = comment}]
                     else
                       [lem, step]
                   end
@@ -295,9 +308,15 @@
                 accum
                 |> (if tainted = [] then
                       (* e.g., trivial, empty proof by Z3 *)
-                      cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
-                        sort_facts (the_list predecessor, []), massage_methods systematic_methods',
-                        ""))
+                      cons (Prove {
+                        qualifiers = if outer then [Show] else [],
+                        obtains = [],
+                        label = no_label,
+                        goal = concl_t,
+                        subproofs = [],
+                        facts = sort_facts (the_list predecessor, []),
+                        proof_methods = massage_methods systematic_methods',
+                        comment = ""})
                     else
                       I)
                 |> rev
@@ -318,7 +337,15 @@
                      else systematic_methods')
                     |> massage_methods
 
-                  fun prove sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "")
+                  fun prove subproofs facts = Prove {
+                    qualifiers = maybe_show outer c,
+                    obtains = [],
+                    label = l,
+                    goal = t,
+                    subproofs = subproofs,
+                    facts = facts,
+                    proof_methods = meths,
+                    comment = ""}
                   fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
                 in
                   if is_clause_tainted c then
@@ -339,7 +366,15 @@
                       (if skolem then
                          (case skolems_of ctxt t of
                            [] => prove [] deps
-                         | skos => Prove ([], skos, l, t, [], deps, meths, ""))
+                         | skos => Prove {
+                             qualifiers = [],
+                             obtains = skos,
+                             label = l,
+                             goal = t,
+                             subproofs = [],
+                             facts = deps,
+                             proof_methods = meths,
+                             comment = ""})
                        else
                          prove [] deps)
                 end
@@ -351,10 +386,15 @@
                   val l = label_of_clause c
                   val t = prop_of_clause c
                   val step =
-                    Prove (maybe_show outer c, [], l, t,
-                      map isar_case (filter_out (null o snd) cases),
-                      sort_facts (the_list predecessor, []), massage_methods systematic_methods',
-                      "")
+                    Prove {
+                      qualifiers = maybe_show outer c,
+                      obtains = [],
+                      label = l,
+                      goal = t,
+                      subproofs = map isar_case (filter_out (null o snd) cases),
+                      facts = sort_facts (the_list predecessor, []),
+                      proof_methods = massage_methods systematic_methods',
+                      comment = ""}
                 in
                   isar_steps outer (SOME l) (step :: accum) infs
                 end
@@ -424,7 +464,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 (_, _, _, _, _, (_, gfs), meth :: _, _)], ...} =>
+                     Proof {steps = [Prove {facts = (_, gfs), proof_methods = meth :: _, ...}],
+                     ...} =>
                      let
                        val used_facts' =
                          map_filter (fn s =>