--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Nov 28 12:25:43 2012 +0100
@@ -7,7 +7,7 @@
signature SLEDGEHAMMER_SHRINK =
sig
- type isar_step = Sledgehammer_Isar_Reconstruct.isar_step
+ type isar_step = Sledgehammer_Proof.isar_step
val shrink_proof :
bool -> Proof.context -> string -> string -> bool -> Time.time -> real
-> isar_step list -> isar_step list * (bool * Time.time)
@@ -16,7 +16,7 @@
structure Sledgehammer_Shrink (* : SLEDGEHAMMER_SHRINK *) =
struct
-open Sledgehammer_Isar_Reconstruct
+open Sledgehammer_Proof
(* Parameters *)
val merge_timeout_slack = 1.2