# HG changeset patch
# User wenzelm
# Date 1449692456 -3600
# Node ID a16497c686cbddb781053f18d808ba48fb992b14
# Parent  b8a3deee50dbf7fd975f36632de266f651683161
tuned;

diff -r b8a3deee50db -r a16497c686cb src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Dec 09 21:15:28 2015 +0100
+++ b/src/Pure/Isar/token.ML	Wed Dec 09 21:20:56 2015 +0100
@@ -64,9 +64,9 @@
   val get_files: T -> file Exn.result list
   val put_files: file Exn.result list -> T -> T
   val get_value: T -> value option
+  val reports_of_value: T -> Position.report list
   val name_value: name_value -> value
   val get_name: T -> name_value option
-  val reports_of_value: T -> Position.report list
   val declare_maxidx: T -> Proof.context -> Proof.context
   val map_facts: (string option -> thm list -> thm list) -> T -> T
   val transform: morphism -> T -> T
@@ -360,25 +360,15 @@
 fun get_value (Token (_, _, Value v)) = v
   | get_value _ = NONE;
 
-fun get_assignable_value (Token (_, _, Assignable r)) = ! r
-  | get_assignable_value (Token (_, _, Value v)) = v
-  | get_assignable_value _ = NONE;
-
 fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
   | map_value _ tok = tok;
 
 
-(* name value *)
-
-fun name_value a = Name (a, Morphism.identity);
+(* reports of value *)
 
-fun get_name tok =
-  (case get_assignable_value tok of
-    SOME (Name (a, _)) => SOME a
-  | _ => NONE);
-
-
-(* reports of value *)
+fun get_assignable_value (Token (_, _, Assignable r)) = ! r
+  | get_assignable_value (Token (_, _, Value v)) = v
+  | get_assignable_value _ = NONE;
 
 fun reports_of_value tok =
   (case get_assignable_value tok of
@@ -394,6 +384,16 @@
   | _ => []);
 
 
+(* name value *)
+
+fun name_value a = Name (a, Morphism.identity);
+
+fun get_name tok =
+  (case get_assignable_value tok of
+    SOME (Name (a, _)) => SOME a
+  | _ => NONE);
+
+
 (* maxidx *)
 
 fun declare_maxidx tok =