src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML

     val enrich_with_assms = fold (uncurry enrich_with_fact)
 
     fun enrich_with_proof (Proof (_, assms, isar_steps)) =
       enrich_with_assms assms #> fold enrich_with_step isar_steps
     and enrich_with_step (Let _) = I
-      | enrich_with_step (Prove (_, _, l, t, subproofs, _)) =
+      | enrich_with_step (Prove (_, _, l, t, subproofs, _, _)) =
         enrich_with_fact l t #> fold enrich_with_proof subproofs
   in
     enrich_with_proof proof ctxt
   end
 

   let
     val thy = Proof_Context.theory_of ctxt
 
     val concl = 
       (case try List.last steps of
-        SOME (Prove (_, [], _, t, _, _)) => t
+        SOME (Prove (_, [], _, t, _, _, _)) => t
       | _ => raise Fail "preplay error: malformed subproof")
 
     val var_idx = maxidx_of_term concl + 1
     fun var_of_free (x, T) = Var ((x, var_idx), T)
     val subst = map (`var_of_free #> swap #> apfst Free) fixed_frees

     | Blast_Method => blast_tac ctxt
     | Algebra_Method => Groebner.algebra_tac [] [] ctxt
     | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
 
 (* main function for preplaying Isar steps; may throw exceptions *)
-fun raw_preplay_step_for_method ctxt timeout meth
-    (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
+fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) =
   let
     val goal =
       (case xs of
         [] => t
       | _ =>

   | add_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2))
   | add_preplay_outcomes play1 play2 =
     Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
 
 fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
-      (step as Prove (_, _, l, _, _, (_, meths))) meths_outcomes0 =
+      (step as Prove (_, _, l, _, _, _, meths)) meths_outcomes0 =
     let
       fun lazy_preplay meth =
         Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step)
       val meths_outcomes = meths_outcomes0
         |> map (apsnd Lazy.value)

 fun fastest_method_of_isar_step preplay_data =
   the o Canonical_Label_Tab.lookup preplay_data
   #> get_best_method_outcome Lazy.force
   #> fst
 
-fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, (_, meths))) =
+fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths)) =
     Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (the_single meths))
   | forced_outcome_of_step _ _ = Played Time.zeroTime
 
 fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) =
   fold_isar_steps (add_preplay_outcomes o forced_outcome_of_step preplay_data) steps