src/HOL/Tools/try0.ML

--- a/src/HOL/Tools/try0.ML	Tue Oct 16 17:47:23 2012 +0200
+++ b/src/HOL/Tools/try0.ML	Tue Oct 16 20:23:00 2012 +0200
@@ -55,7 +55,7 @@
   #> 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")
+  #> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source")
 
 fun apply_named_method_on_first_goal method thy =
   method |> parse_method