tuned signature;

--- a/src/Pure/Isar/proof_context.ML	Fri Mar 09 17:24:42 2012 +0000
+++ b/src/Pure/Isar/proof_context.ML	Fri Mar 09 20:04:19 2012 +0100
@@ -839,7 +839,7 @@
 
 fun retrieve_thms pick ctxt (Facts.Fact s) =
       let
-        val (_, pos) = Syntax.read_token s;
+        val pos = Syntax.read_token_pos s;
         val prop =
           Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
           |> singleton (Variable.polymorphic ctxt);

--- a/src/Pure/Syntax/syntax.ML	Fri Mar 09 17:24:42 2012 +0000
+++ b/src/Pure/Syntax/syntax.ML	Fri Mar 09 20:04:19 2012 +0100
@@ -15,6 +15,7 @@
   val ambiguity_limit_raw: Config.raw
   val ambiguity_limit: int Config.T
   val read_token: string -> Symbol_Pos.T list * Position.T
+  val read_token_pos: string -> Position.T
   val parse_token: Proof.context -> (XML.tree list -> 'a) ->
     Markup.T -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
   val parse_sort: Proof.context -> string -> sort
@@ -164,18 +165,19 @@
 
 (* outer syntax token -- with optional YXML content *)
 
+fun token_position (XML.Elem ((name, props), _)) =
+      if name = Isabelle_Markup.tokenN then Position.of_properties props
+      else Position.none
+  | token_position (XML.Text _) = Position.none;
+
 fun explode_token tree =
   let
     val text = XML.content_of [tree];
-    val pos =
-      (case tree of
-        XML.Elem ((name, props), _) =>
-          if name = Isabelle_Markup.tokenN then Position.of_properties props
-          else Position.none
-      | XML.Text _ => Position.none);
+    val pos = token_position tree;
   in (Symbol_Pos.explode (text, pos), pos) end;
 
 fun read_token str = explode_token (YXML.parse str handle Fail msg => error msg);
+fun read_token_pos str = token_position (YXML.parse str handle Fail msg => error msg);
 
 fun parse_token ctxt decode markup parse str =
   let

--- a/src/Tools/induct_tacs.ML	Fri Mar 09 17:24:42 2012 +0000
+++ b/src/Tools/induct_tacs.ML	Fri Mar 09 20:04:19 2012 +0100
@@ -35,7 +35,7 @@
       | NONE =>
           (case Induct.find_casesT ctxt
               (#2 (check_type ctxt (Proof_Context.read_term_schematic ctxt s,
-                #2 (Syntax.read_token s)))) of
+                Syntax.read_token_pos s))) of
             rule :: _ => rule
           | [] => @{thm case_split}));
     val _ = Method.trace ctxt [rule];
@@ -72,7 +72,7 @@
     fun induct_var name =
       let
         val t = Syntax.read_term ctxt name;
-        val (_, pos) = Syntax.read_token name;
+        val pos = Syntax.read_token_pos name;
         val (x, _) = Term.dest_Free t handle TERM _ =>
           error ("Induction argument not a variable: " ^
             Syntax.string_of_term ctxt t ^ Position.str_of pos);