diff -r e9812a95d108 -r 35ec3757d3c1 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Dec 22 21:58:27 2015 +0100
+++ b/src/Pure/Isar/method.ML	Wed Dec 23 14:40:18 2015 +0100
@@ -73,6 +73,7 @@
   val check_name: Proof.context -> xstring * Position.T -> string
   val check_src: Proof.context -> Token.src -> Token.src
   val check_text: Proof.context -> text -> text
+  val checked_text: text -> bool
   val method_syntax: (Proof.context -> method) context_parser ->
     Token.src -> Proof.context -> method
   val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
@@ -439,6 +440,10 @@
   | check_text _ (Basic m) = Basic m
   | check_text ctxt (Combinator (x, y, body)) = Combinator (x, y, map (check_text ctxt) body);
 
+fun checked_text (Source src) = Token.checked_src src
+  | checked_text (Basic _) = true
+  | checked_text (Combinator (_, _, body)) = forall checked_text body;
+
 
 (* method setup *)