--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Fri Jan 31 16:10:39 2014 +0100
@@ -9,9 +9,9 @@
signature SLEDGEHAMMER_ISAR_TRY0 =
sig
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
- type preplay_interface = Sledgehammer_Isar_Preplay.preplay_interface
+ type preplay_data = Sledgehammer_Isar_Preplay.preplay_data
- val try0 : Time.time -> preplay_interface -> isar_proof -> isar_proof
+ val try0_isar_proof : Time.time -> preplay_data -> isar_proof -> isar_proof
end;
structure Sledgehammer_Isar_Try0 : SLEDGEHAMMER_ISAR_TRY0 =
@@ -30,7 +30,7 @@
fun try0_step _ _ (step as Let _) = step
| try0_step preplay_timeout
- ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_interface)
+ ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_data)
(step as Prove (_, _, l, _, _, _)) =
let
val timeout =
@@ -48,6 +48,6 @@
| NONE => step)
end
-val try0 = map_isar_steps oo try0_step
+val try0_isar_proof = map_isar_steps oo try0_step
end;