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