--- a/src/Pure/Isar/attrib.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/Isar/attrib.ML Tue Nov 11 18:16:25 2014 +0100
@@ -210,7 +210,7 @@
(ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
ML_Lex.read_source false source @
ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
- |> ML_Context.expression (#pos source)
+ |> ML_Context.expression (#range source)
"val (name, scan, comment): binding * attribute context_parser * string"
"Context.map_proof (Attrib.local_setup name scan comment)"
|> Context.proof_map;
@@ -293,7 +293,7 @@
in
(case Token.read_no_commands keywords Parse.attribs syms of
[raw_srcs] => check_attribs ctxt raw_srcs
- | _ => error ("Malformed attributes" ^ Position.here (#pos source)))
+ | _ => error ("Malformed attributes" ^ Position.here (#1 (#range source))))
end;