src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -21,7 +21,7 @@
      preplay_quietly: Time.time -> isar_step -> play_outcome,
      overall_preplay_outcome: isar_proof -> play_outcome}
 
-  val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> bool -> Time.time ->
+  val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> Time.time ->
     isar_proof -> isar_preplay_data
 end;
 
@@ -172,67 +172,60 @@
 
    Precondition: The proof must be labeled canonically; cf.
    "Slegehammer_Isar_Proof.relabel_isar_proof_canonically". *)
-fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
-  if not do_preplay then
-    (* the "dont_preplay" option pretends that everything works just fine *)
-    {set_preplay_outcomes = K (K ()),
-     preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
-     preplay_quietly = K (K (Played Time.zeroTime)),
-     overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
-  else
-    let
-      val ctxt = enrich_context_with_local_facts proof ctxt
+fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans preplay_timeout proof =
+  let
+    val ctxt = enrich_context_with_local_facts proof ctxt
 
-      fun preplay quietly timeout meth step =
-        preplay_raw debug type_enc lam_trans ctxt timeout meth step
-        handle exn =>
-          if Exn.is_interrupt exn then
-            reraise exn
-          else
-            (if not quietly andalso debug then
-               warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^ @{make_string} exn)
-             else
-               ();
-             Play_Failed)
+    fun preplay quietly timeout meth step =
+      preplay_raw debug type_enc lam_trans ctxt timeout meth step
+      handle exn =>
+        if Exn.is_interrupt exn then
+          reraise exn
+        else
+          (if not quietly andalso debug then
+             warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^ @{make_string} exn)
+           else
+             ();
+           Play_Failed)
 
-      (* preplay steps treating exceptions like timeouts *)
-      fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, meth :: _))) =
-          preplay true timeout meth step
-        | preplay_quietly _ _ = Played Time.zeroTime
+    (* preplay steps treating exceptions like timeouts *)
+    fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, meth :: _))) =
+        preplay true timeout meth step
+      | preplay_quietly _ _ = Played Time.zeroTime
 
-      val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
+    val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
+
+    fun set_preplay_outcomes l meths_outcomes =
+      preplay_tab := Canonical_Label_Tab.map_entry l (fold (AList.update (op =)) meths_outcomes)
+        (!preplay_tab)
 
-      fun set_preplay_outcomes l meths_outcomes =
-        preplay_tab := Canonical_Label_Tab.map_entry l (fold (AList.update (op =)) meths_outcomes)
-          (!preplay_tab)
+    fun preplay_outcome l meth =
+      (case Canonical_Label_Tab.lookup (!preplay_tab) l of
+        SOME meths_outcomes =>
+        (case AList.lookup (op =) meths_outcomes meth of
+          SOME outcome => outcome
+        | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
+      | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
 
-      fun preplay_outcome l meth =
-        (case Canonical_Label_Tab.lookup (!preplay_tab) l of
-          SOME meths_outcomes =>
-          (case AList.lookup (op =) meths_outcomes meth of
-            SOME outcome => outcome
-          | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
-        | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
-
-      fun result_of_step (Prove (_, _, l, _, _, (_, meth :: _))) =
-          Lazy.force (preplay_outcome l meth)
-        | result_of_step _ = Played Time.zeroTime
+    fun result_of_step (Prove (_, _, l, _, _, (_, meth :: _))) =
+        Lazy.force (preplay_outcome l meth)
+      | result_of_step _ = Played Time.zeroTime
 
-      fun overall_preplay_outcome (Proof (_, _, steps)) =
-        fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
+    fun overall_preplay_outcome (Proof (_, _, steps)) =
+      fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
 
-      fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
-          preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
-              (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths)
-            (!preplay_tab)
-        | reset_preplay_outcomes _ = ()
+    fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
+        preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
+            (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths)
+          (!preplay_tab)
+      | reset_preplay_outcomes _ = ()
 
-      val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
-    in
-      {set_preplay_outcomes = set_preplay_outcomes,
-       preplay_outcome = preplay_outcome,
-       preplay_quietly = preplay_quietly,
-       overall_preplay_outcome = overall_preplay_outcome}
-    end
+    val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
+  in
+    {set_preplay_outcomes = set_preplay_outcomes,
+     preplay_outcome = preplay_outcome,
+     preplay_quietly = preplay_quietly,
+     overall_preplay_outcome = overall_preplay_outcome}
+  end
 
 end;