--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jun 22 16:56:03 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jun 22 16:56:03 2015 +0200
@@ -66,6 +66,11 @@
fun is_metis_method (Metis_Method _) = true
| is_metis_method _ = false
+fun add_chained [] t = t
+ | add_chained chained ((t as Const (@{const_name Pure.all}, _)) $ Abs (s, T, u)) =
+ t $ Abs (s, T, add_chained chained u)
+ | add_chained chained t = Logic.list_implies (chained, t)
+
fun play_one_line_proof minimize timeout used_facts state i (preferred_meth, methss) =
if timeout = Time.zeroTime then
(used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
@@ -73,11 +78,10 @@
let
val ctxt = Proof.context_of state
+ val fact_names = map fst used_facts
val {facts = chained, goal, ...} = Proof.goal state
- val fact_names = map fst used_facts
-
- val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
- val goal_t = Logic.list_implies (map Thm.prop_of chained @ hyp_ts, concl_t)
+ val goal_t = Logic.get_goal (Thm.prop_of goal) i
+ |> add_chained (map Thm.prop_of chained)
fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
| try_methss ress [] =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Jun 22 16:56:03 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Jun 22 16:56:03 2015 +0200
@@ -132,7 +132,7 @@
(case xs of
[] => t
| _ =>
- (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
+ (* proof obligation: !!thesis. (!!x1...xn. t ==> thesis) ==> thesis
(cf. "~~/src/Pure/Isar/obtain.ML") *)
let
val frees = map Free xs
@@ -140,10 +140,10 @@
Free (singleton (Variable.variant_frees ctxt frees) ("thesis", HOLogic.boolT))
val thesis_prop = HOLogic.mk_Trueprop thesis
- (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
+ (* !!x1...xn. t ==> thesis *)
val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
in
- (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
+ (* !!thesis. (!!x1...xn. t ==> thesis) ==> thesis *)
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
end)