src/HOL/Tools/try0.ML
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