1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Mar 09 21:50:27 2012 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Mar 09 22:05:15 2012 +0100
     1.3 @@ -839,7 +839,7 @@
     1.4  
     1.5  fun retrieve_thms pick ctxt (Facts.Fact s) =
     1.6        let
     1.7 -        val (_, pos) = Syntax.read_token s;
     1.8 +        val pos = Syntax.read_token_pos s;
     1.9          val prop =
    1.10            Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
    1.11            |> singleton (Variable.polymorphic ctxt);

     2.1 --- a/src/Pure/Syntax/syntax.ML	Fri Mar 09 21:50:27 2012 +0100
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Mar 09 22:05:15 2012 +0100
     2.3 @@ -15,6 +15,7 @@
     2.4    val ambiguity_limit_raw: Config.raw
     2.5    val ambiguity_limit: int Config.T
     2.6    val read_token: string -> Symbol_Pos.T list * Position.T
     2.7 +  val read_token_pos: string -> Position.T
     2.8    val parse_token: Proof.context -> (XML.tree list -> 'a) ->
     2.9      Markup.T -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
    2.10    val parse_sort: Proof.context -> string -> sort
    2.11 @@ -164,18 +165,19 @@
    2.12  
    2.13  (* outer syntax token -- with optional YXML content *)
    2.14  
    2.15 +fun token_position (XML.Elem ((name, props), _)) =
    2.16 +      if name = Isabelle_Markup.tokenN then Position.of_properties props
    2.17 +      else Position.none
    2.18 +  | token_position (XML.Text _) = Position.none;
    2.19 +
    2.20  fun explode_token tree =
    2.21    let
    2.22      val text = XML.content_of [tree];
    2.23 -    val pos =
    2.24 -      (case tree of
    2.25 -        XML.Elem ((name, props), _) =>
    2.26 -          if name = Isabelle_Markup.tokenN then Position.of_properties props
    2.27 -          else Position.none
    2.28 -      | XML.Text _ => Position.none);
    2.29 +    val pos = token_position tree;
    2.30    in (Symbol_Pos.explode (text, pos), pos) end;
    2.31  
    2.32  fun read_token str = explode_token (YXML.parse str handle Fail msg => error msg);
    2.33 +fun read_token_pos str = token_position (YXML.parse str handle Fail msg => error msg);
    2.34  
    2.35  fun parse_token ctxt decode markup parse str =
    2.36    let

     3.1 --- a/src/Tools/induct_tacs.ML	Fri Mar 09 21:50:27 2012 +0100
     3.2 +++ b/src/Tools/induct_tacs.ML	Fri Mar 09 22:05:15 2012 +0100
     3.3 @@ -35,7 +35,7 @@
     3.4        | NONE =>
     3.5            (case Induct.find_casesT ctxt
     3.6                (#2 (check_type ctxt (Proof_Context.read_term_schematic ctxt s,
     3.7 -                #2 (Syntax.read_token s)))) of
     3.8 +                Syntax.read_token_pos s))) of
     3.9              rule :: _ => rule
    3.10            | [] => @{thm case_split}));
    3.11      val _ = Method.trace ctxt [rule];
    3.12 @@ -72,7 +72,7 @@
    3.13      fun induct_var name =
    3.14        let
    3.15          val t = Syntax.read_term ctxt name;
    3.16 -        val (_, pos) = Syntax.read_token name;
    3.17 +        val pos = Syntax.read_token_pos name;
    3.18          val (x, _) = Term.dest_Free t handle TERM _ =>
    3.19            error ("Induction argument not a variable: " ^
    3.20              Syntax.string_of_term ctxt t ^ Position.str_of pos);