src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML

   type isar_proof = Sledgehammer_Isar_Proof.isar_proof
   type label = Sledgehammer_Isar_Proof.label
 
   val trace : bool Config.T
 
-  type preplay_data =
+  type isar_preplay_data =
     {get_preplay_outcome: label -> play_outcome,
      set_preplay_outcome: label -> play_outcome -> unit,
      preplay_quietly: Time.time -> isar_step -> play_outcome,
      overall_preplay_outcome: isar_proof -> play_outcome}
 
-  val proof_preplay_data : bool -> Proof.context -> string -> string -> bool -> Time.time ->
-    isar_proof -> preplay_data
+  val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> bool -> Time.time ->
+    isar_proof -> isar_preplay_data
 end;
 
 structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY =
 struct
 

     end
 
 
 (*** proof preplay interface ***)
 
-type preplay_data =
+type isar_preplay_data =
   {get_preplay_outcome: label -> play_outcome,
    set_preplay_outcome: label -> play_outcome -> unit,
    preplay_quietly: Time.time -> isar_step -> play_outcome,
    overall_preplay_outcome: isar_proof -> play_outcome}
 

 (* Given a proof, produces an imperative preplay interface with a shared table mapping from labels
    to preplay results. The preplay results are caluclated lazyly and cached to avoid repeated
    calculation.
 
    Precondition: The proof must be labeled canonically; cf.
-   "Slegehammer_Proof.relabel_proof_canonically". *)
-fun proof_preplay_data debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
+   "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 *)
     {get_preplay_outcome = K (Played Time.zeroTime),
      set_preplay_outcome = K (K ()),
      preplay_quietly = K (K (Played Time.zeroTime)),
-     overall_preplay_outcome = K (Played Time.zeroTime)} : preplay_data
+     overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
   else
     let
       val ctxt = enrich_context_with_local_facts proof ctxt
 
       fun preplay quietly timeout step =