--- a/src/HOL/Eisbach/method_closure.ML Fri Apr 01 17:13:40 2016 +0200
+++ b/src/HOL/Eisbach/method_closure.ML Fri Apr 01 17:14:27 2016 +0200
@@ -85,8 +85,7 @@
SOME (text, range) =>
if Method.checked_text text then text
else (Method.report (text, range); Method.check_text ctxt text)
- | NONE =>
- error ("Failed to parse method" ^ Position.here (Position.set_range (Token.range_of src))));
+ | NONE => error ("Failed to parse method" ^ Position.here (#1 (Token.range_of src))));
fun read_closure ctxt src0 =
let
--- a/src/Pure/Isar/attrib.ML Fri Apr 01 17:13:40 2016 +0200
+++ b/src/Pure/Isar/attrib.ML Fri Apr 01 17:14:27 2016 +0200
@@ -153,9 +153,7 @@
let
val _ =
if Token.checked_src src then ()
- else
- Context_Position.report ctxt
- (Position.set_range (Token.range_of src)) Markup.language_attribute;
+ else Context_Position.report ctxt (#1 (Token.range_of src)) Markup.language_attribute;
in #1 (Token.check_src ctxt get_attributes src) end;
val attribs =
--- a/src/Pure/Isar/method.ML Fri Apr 01 17:13:40 2016 +0200
+++ b/src/Pure/Isar/method.ML Fri Apr 01 17:14:27 2016 +0200
@@ -621,7 +621,7 @@
Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd;
val modifier_report =
- (Position.set_range (Token.range_of modifier_toks),
+ (#1 (Token.range_of modifier_toks),
Markup.properties (Position.def_properties_of pos)
(Markup.entity Markup.method_modifierN ""));
val _ =
@@ -747,7 +747,7 @@
if detect_closure_state st then NONE
else
SOME (fn () => ("Excessive case name(s): " ^ commas_quote (map Token.content_of bad) ^
- Position.here (Position.set_range (Token.range_of bad)))))
+ Position.here (#1 (Token.range_of bad)))))
|> (fn SOME msg => Seq.single (Seq.Error msg)
| NONE => goal_cases_tac (map Token.content_of names) (ctxt, st)))))
"bind cases for goals" #>
--- a/src/Pure/Syntax/syntax_ext.ML Fri Apr 01 17:13:40 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Fri Apr 01 17:14:27 2016 +0200
@@ -250,8 +250,7 @@
Scan.repeat1 scan_delim_char >> (Delim o Symbol_Pos.content);
val scan_symb =
- Scan.trace scan_sym >>
- (fn (syms, trace) => SOME (syms, Position.set_range (Symbol_Pos.range trace))) ||
+ Scan.trace scan_sym >> (fn (syms, trace) => SOME (syms, #1 (Symbol_Pos.range trace))) ||
$$ "'" -- scan_one Symbol.is_blank >> K NONE;
val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'");