src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -52,9 +52,9 @@
 
     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, _, _)) =
+    and enrich_with_step (Prove (_, _, l, t, subproofs, _, _, _)) =
         enrich_with_fact l t #> fold enrich_with_proof subproofs
+      | enrich_with_step _ = I
   in
     enrich_with_proof proof ctxt
   end
@@ -88,7 +88,7 @@
 
     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
@@ -100,8 +100,8 @@
     |> Skip_Proof.make_thm thy
   end
 
-(* main function for preplaying Isar steps; may throw exceptions *)
-fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) =
+(* may throw exceptions *)
+fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, facts, _, _)) =
   let
     val goal =
       (case xs of
@@ -122,18 +122,18 @@
           Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
         end)
 
-    val facts =
-      resolve_fact_names ctxt fact_names
+    val assmsp =
+      resolve_fact_names ctxt facts
       |>> append (map (thm_of_proof ctxt) subproofs)
 
     fun prove () =
       Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
-        HEADGOAL (tac_of_proof_method ctxt facts meth))
+        HEADGOAL (tac_of_proof_method ctxt assmsp meth))
       handle ERROR msg => error ("Preplay error: " ^ msg)
 
     val play_outcome = take_time timeout prove ()
   in
-    (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else ();
+    (if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else ();
      play_outcome)
   end
 
@@ -164,7 +164,7 @@
     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)
@@ -207,7 +207,7 @@
   #> 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 (hd meths))
   | forced_outcome_of_step _ _ = Played Time.zeroTime