# HG changeset patch
# User wenzelm
# Date 1459523667 -7200
# Node ID 063d2f23cdf64f2302b9d4282c3ce71ccd94d99b
# Parent  c4fa2b38159120811285eb2fb0bd693b258e41b6
removed redundant Position.set_range -- already done in Position.range;

diff -r c4fa2b381591 -r 063d2f23cdf6 src/HOL/Eisbach/method_closure.ML
--- 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
diff -r c4fa2b381591 -r 063d2f23cdf6 src/Pure/Isar/attrib.ML
--- 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 =
diff -r c4fa2b381591 -r 063d2f23cdf6 src/Pure/Isar/method.ML
--- 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" #>
diff -r c4fa2b381591 -r 063d2f23cdf6 src/Pure/Syntax/syntax_ext.ML
--- 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 (~$$ "'");