--- a/src/HOL/Tools/try0.ML Tue Aug 12 18:54:53 2014 +0200
+++ b/src/HOL/Tools/try0.ML Tue Aug 12 20:18:27 2014 +0200
@@ -48,12 +48,12 @@
NONE
end;
-val parse_method =
- enclose "(" ")"
- #> Outer_Syntax.scan Position.start
- #> filter Token.is_proper
- #> Scan.read Token.stopper Method.parse
- #> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
+fun parse_method s =
+ enclose "(" ")" s
+ |> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.start
+ |> filter Token.is_proper
+ |> Scan.read Token.stopper Method.parse
+ |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
fun apply_named_method_on_first_goal ctxt =
parse_method