| changeset 55997 | 9dc5ce83202c |
| parent 55765 | ec7ca5388dea |
| child 56027 | 25889f5c39a8 |
--- a/src/HOL/Tools/try0.ML Sat Mar 08 13:49:01 2014 +0100 +++ b/src/HOL/Tools/try0.ML Sat Mar 08 21:08:10 2014 +0100 @@ -57,8 +57,7 @@ fun apply_named_method_on_first_goal ctxt = parse_method - #> Method.check_source ctxt - #> Method.the_method ctxt + #> Method.method_cmd ctxt #> Method.Basic #> (fn m => Method.Select_Goals (Method.no_combinator_info, 1, m)) #> Proof.refine;