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, l, t, By_Metis (subproofs, facts))) =
-        add_step_pre ind qs subproofs
-        #> add_suffix (of_prove qs (length subproofs) ^ " ")
-        #> add_step_post ind l t facts ""
-      | add_step ind (Obtain (qs, Fix xs, l, t, By_Metis (subproofs, facts))) =
-        add_step_pre ind qs subproofs
-        #> add_suffix (of_obtain qs (length subproofs) ^ " ")
-        #> add_frees xs
-        #> add_suffix " where "
-        (* The new skolemizer puts the arguments in the same order as the ATPs
-           (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding
-           Vampire). *)
-        #> add_step_post ind l t facts
-               (if exists (fn (_, T) => length (binder_types T) > 1) xs then
-                  "using [[metis_new_skolem]] "
-                else
-                  "")
+      | add_step ind (Prove (qs, Fix xs, l, t, By_Metis (subproofs, 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 ""
+        | _ => (* obtain *)
+            add_step_pre ind qs subproofs
+            #> add_suffix (of_obtain qs (length subproofs) ^ " ")
+            #> add_frees xs
+            #> add_suffix " where "
+            (* The new skolemizer puts the arguments in the same order as the
+               ATPs (E and Vampire -- but see also "atp_proof_reconstruct.ML"
+               regarding Vampire). *)
+            #> add_step_post ind l t facts
+                 (if exists (fn (_, T) => length (binder_types T) > 1) xs then
+                    "using [[metis_new_skolem]] "
+                  else
+                    ""))
     and add_steps ind = fold (add_step ind)
     and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) =
       ("", ctxt)
       |> add_fix ind xs
       |> add_assms ind assms

       |> fst
   in
     (* One-step proofs are pointless; better use the Metis one-liner
        directly. *)
     case proof of
-      Proof (Fix [], Assume [], [Prove (_, _, _, By_Metis ([], _))]) => ""
+      Proof (Fix [], Assume [], [Prove (_, Fix [], _, _, By_Metis ([], _))]) => ""
     | _ => (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 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 (Obtain (qs, xs, l, t, By_Metis (subproofs, facts))) =
-          Obtain (qs, xs, do_label l, t, By_Metis (map do_proof subproofs, facts))
-      | do_step (Prove (qs, l, t, By_Metis (subproofs, facts))) =
-          Prove (qs, do_label l, t, By_Metis (map do_proof subproofs, facts))
+    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))
       | 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 (Obtain (qs, xs, l, t, by) :: steps) =
+      | do_steps subst depth next (Prove (qs, xs, l, t, by) :: steps) =
         let
           val (l, subst, next) =
             (l, subst, next) |> fresh_label depth have_prefix
           val by = by |> do_byline subst depth
-        in Obtain (qs, xs, l, t, by) :: do_steps subst depth next steps end
-      | do_steps subst depth next (Prove (qs, l, t, by) :: steps) =
-        let
-          val (l, subst, next) =
-            (l, subst, next) |> fresh_label depth have_prefix
-          val by = by |> do_byline subst depth
-        in Prove (qs, l, t, by) :: do_steps subst depth next steps end
+        in Prove (qs, xs, l, t, 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)

   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 (Obtain (qs, xs, l, t,
+    fun chain_step lbl (Prove (qs, xs, l, t,
                                 By_Metis (subproofs, (lfs, gfs)))) =
-        let val (qs', lfs) = do_qs_lfs lbl lfs in
-          Obtain (qs' @ qs, xs, l, t,
-            By_Metis (chain_proofs subproofs, (lfs, gfs)))
-        end
-      | chain_step lbl (Prove (qs, l, t, By_Metis (subproofs, (lfs, gfs)))) =
-        let val (qs', lfs) = do_qs_lfs lbl lfs in
-          Prove (qs' @ qs, l, t, By_Metis (chain_proofs subproofs, (lfs, gfs)))
-        end
+          let val (qs', lfs) = do_qs_lfs lbl lfs in
+            Prove (qs' @ qs, xs, l, t,
+              By_Metis (chain_proofs subproofs, (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
       | chain_steps _ (i :: is) = i :: chain_steps (label_of_step i) is

             fun skolems_of t =
               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 [], no_label,
-                                   concl_t,
+                      cons (Prove (if outer then [Show] else [],
+                                   Fix [], no_label, concl_t,
                                    By_Metis ([], ([the predecessor], []))))
                     else
                       I)
                 |> rev
               | do_steps outer _ accum (Have (gamma, c) :: infs) =

                   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 [], l, t, by)
+                  fun prove by = Prove (maybe_show outer c [], Fix [], l, t, by)
                   fun do_rest l step =
                     do_steps outer (SOME l) (step :: accum) infs
                 in
                   if is_clause_tainted c then
                     case gamma of

                       else
                         do_rest l (prove by)
                     | _ => do_rest l (prove by)
                   else
                     if is_clause_skolemize_rule c then
-                      do_rest l (Obtain ([], Fix (skolems_of t), l, t, by))
+                      do_rest l (Prove ([], Fix (skolems_of t), l, t, by))
                     else
                       do_rest l (prove by)
                 end
               | do_steps outer predecessor accum (Cases cases :: infs) =
                 let

                              infs
                   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 [], l, t,
+                    Prove (maybe_show outer c [], Fix [], l, t,
                       By_Metis (map do_case cases, (the_list predecessor, [])))
                 in
                   do_steps outer (SOME l) (step :: accum) infs
                 end
             and do_proof outer fix assms infs =