--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Mar 28 12:05:47 2016 +0200
@@ -49,7 +49,8 @@
goal : thm,
subgoal : int,
subgoal_count : int,
- factss : (string * fact list) list}
+ factss : (string * fact list) list,
+ found_proof : unit -> unit}
type prover_result =
{outcome : atp_failure option,
@@ -133,7 +134,8 @@
goal : thm,
subgoal : int,
subgoal_count : int,
- factss : (string * fact list) list}
+ factss : (string * fact list) list,
+ found_proof : unit -> unit}
type prover_result =
{outcome : atp_failure option,