src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

         add_suffix (of_indent ind ^ "let ")
         #> add_term t1
         #> add_suffix " = "
         #> add_term t2
         #> add_suffix "\n"
-      | add_step ind (Prove (qs, Fix xs, l, t, By_Metis (subproofs, facts))) =
+      | add_step ind (Prove (qs, Fix xs, l, t, subproofs, By_Metis facts)) =
         (case xs of
           [] => (* have *)
             add_step_pre ind qs subproofs
             #> add_suffix (of_prove qs (length subproofs) ^ " ")
             #> add_step_post ind l t facts ""

       |> fst
   in
     (* One-step proofs are pointless; better use the Metis one-liner
        directly. *)
     case proof of
-      Proof (Fix [], Assume [], [Prove (_, Fix [], _, _, By_Metis ([], _))]) => ""
+      Proof (Fix [], Assume [], [Prove (_, Fix [], _, _, [], _)]) => ""
     | _ => (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
             of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
             of_indent 0 ^ (if n <> 1 then "next" else "qed")
   end
 
-fun add_labels_of_step step =
-  case byline_of_step step of
-    NONE => I
-  | SOME (By_Metis (subproofs, (ls, _))) =>
-    union (op =) ls #> fold add_labels_of_proof subproofs
-and add_labels_of_proof proof = fold add_labels_of_step (steps_of_proof proof)
+val add_labels_of_proof =
+  steps_of_proof #> fold_isar_steps
+    (byline_of_step #> (fn SOME (By_Metis (ls, _)) => union (op =) ls
+                         | _ => I))
 
 fun kill_useless_labels_in_proof proof =
   let
     val used_ls = add_labels_of_proof proof []
     fun do_label l = if member (op =) used_ls l then l else no_label
     fun do_assms (Assume assms) = Assume (map (apfst do_label) assms)
-    fun do_step (Prove (qs, xs, l, t, By_Metis (subproofs, facts))) =
-          Prove (qs, xs, do_label l, t, By_Metis (map do_proof subproofs, facts))
+    fun do_step (Prove (qs, xs, l, t, subproofs, by)) =
+          Prove (qs, xs, do_label l, t, map do_proof subproofs, by)
       | do_step step = step
     and do_proof (Proof (fix, assms, steps)) =
           Proof (fix, do_assms assms, map do_step steps)
   in do_proof proof end
 

     fun do_assms subst depth (Assume assms) =
       fold_map (do_assm depth) assms (subst, 1)
       |> apfst Assume
       |> apsnd fst
     fun do_steps _ _ _ [] = []
-      | do_steps subst depth next (Prove (qs, xs, l, t, by) :: steps) =
+      | do_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) =
         let
           val (l, subst, next) =
             (l, subst, next) |> fresh_label depth have_prefix
+          val sub = do_proofs subst depth sub
           val by = by |> do_byline subst depth
-        in Prove (qs, xs, l, t, by) :: do_steps subst depth next steps end
+        in Prove (qs, xs, l, t, sub, by) :: do_steps subst depth next steps end
       | do_steps subst depth next (step :: steps) =
         step :: do_steps subst depth next steps
     and do_proof subst depth (Proof (fix, assms, steps)) =
       let val (assms, subst) = do_assms subst depth assms in
         Proof (fix, assms, do_steps subst depth 1 steps)
       end
-    and do_byline subst depth (By_Metis (subproofs, facts)) =
-      By_Metis (do_proofs subst depth subproofs, do_facts subst facts)
+    and do_byline subst depth (By_Metis facts) =
+      By_Metis (do_facts subst facts)
     and do_proofs subst depth = map (do_proof subst (depth + 1))
   in do_proof [] 0 end
 
 val chain_direct_proof =
   let
     fun do_qs_lfs NONE lfs = ([], lfs)
       | do_qs_lfs (SOME l0) lfs =
         if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0)
         else ([], lfs)
-    fun chain_step lbl (Prove (qs, xs, l, t,
-                                By_Metis (subproofs, (lfs, gfs)))) =
+    fun chain_step lbl (Prove (qs, xs, l, t, subproofs, By_Metis (lfs, gfs))) =
           let val (qs', lfs) = do_qs_lfs lbl lfs in
-            Prove (qs' @ qs, xs, l, t,
-              By_Metis (chain_proofs subproofs, (lfs, gfs)))
+            Prove (qs' @ qs, xs, l, t, chain_proofs subproofs,
+                   By_Metis (lfs, gfs))
           end
       | chain_step _ step = step
     and chain_steps _ [] = []
       | chain_steps (prev as SOME _) (i :: is) =
         chain_step prev i :: chain_steps (label_of_step i) is

               Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
             fun do_steps outer predecessor accum [] =
                 accum
                 |> (if tainted = [] then
                       cons (Prove (if outer then [Show] else [],
-                                   Fix [], no_label, concl_t,
-                                   By_Metis ([], ([the predecessor], []))))
+                                   Fix [], no_label, concl_t, [],
+                                   By_Metis ([the predecessor], [])))
                     else
                       I)
                 |> rev
               | do_steps outer _ accum (Have (gamma, c) :: infs) =
                 let
                   val l = label_of_clause c
                   val t = prop_of_clause c
                   val by =
-                    By_Metis ([],
-                      (fold (add_fact_of_dependencies fact_names)
-                            gamma no_facts))
-                  fun prove by = Prove (maybe_show outer c [], Fix [], l, t, by)
+                    By_Metis
+                      (fold (add_fact_of_dependencies fact_names) gamma no_facts)
+                  fun prove sub by =
+                    Prove (maybe_show outer c [], Fix [], l, t, sub, by)
                   fun do_rest l step =
                     do_steps outer (SOME l) (step :: accum) infs
                 in
                   if is_clause_tainted c then
                     case gamma of

                           val subproof =
                             Proof (Fix (skolems_of (prop_of_clause g)),
                                    Assume [], rev accum)
                         in
                           do_steps outer (SOME l)
-                              [prove (By_Metis ([subproof], no_facts))] []
+                              [prove [subproof] (By_Metis no_facts)] []
                         end
                       else
-                        do_rest l (prove by)
-                    | _ => do_rest l (prove by)
+                        do_rest l (prove [] by)
+                    | _ => do_rest l (prove [] by)
                   else
                     if is_clause_skolemize_rule c then
-                      do_rest l (Prove ([], Fix (skolems_of t), l, t, by))
+                      do_rest l (Prove ([], Fix (skolems_of t), l, t, [], by))
                     else
-                      do_rest l (prove by)
+                      do_rest l (prove [] by)
                 end
               | do_steps outer predecessor accum (Cases cases :: infs) =
                 let
                   fun do_case (c, infs) =
                     do_proof false [] [(label_of_clause c, prop_of_clause c)]

                   val c = succedent_of_cases cases
                   val l = label_of_clause c
                   val t = prop_of_clause c
                   val step =
                     Prove (maybe_show outer c [], Fix [], l, t,
-                      By_Metis (map do_case cases, (the_list predecessor, [])))
+                      map do_case cases, By_Metis (the_list predecessor, []))
                 in
                   do_steps outer (SOME l) (step :: accum) infs
                 end
             and do_proof outer fix assms infs =
               Proof (Fix fix, Assume assms, do_steps outer NONE [] infs)