--- a/src/HOL/Tools/try0.ML Mon Nov 18 12:35:44 2024 +0100
+++ b/src/HOL/Tools/try0.ML Mon Nov 18 13:30:02 2024 +0100
@@ -74,19 +74,16 @@
val ctxt = Proof.context_of st
- val using_text =
- (K (Method.insert (Attrib.eval_thms ctxt unused)))
- |> Method.Basic
-
val text =
name ^ attrs
|> parse_method ctxt
|> Method.method_cmd ctxt
|> Method.Basic
|> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m]))
- |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Then, [using_text, m]))
- val apply = text |> Proof.refine #> Seq.filter_results
+ val apply =
+ Proof.using [Attrib.eval_thms ctxt unused |> map (rpair [] o single)]
+ #> Proof.refine text #> Seq.filter_results
val num_before = num_goals st
val multiple_goals = all_goals andalso num_before > 1
val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt apply st