| changeset 58005 | c28e6bc6635d |
| parent 57918 | f5d73caba4e5 |
| child 58011 | bc6bced136e5 |
--- a/src/HOL/Tools/try0.ML Tue Aug 19 15:10:37 2014 +0200 +++ b/src/HOL/Tools/try0.ML Tue Aug 19 15:55:06 2014 +0200 @@ -59,7 +59,7 @@ parse_method #> Method.method_cmd ctxt #> Method.Basic - #> (fn m => Method.Select_Goals (Method.no_combinator_info, 1, m)) + #> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m])) #> Proof.refine; fun add_attr_text (NONE, _) s = s