# HG changeset patch
# User wenzelm
# Date 1449691089 -3600
# Node ID 7e020220561a320ad98bc7abd50e1f562631265e
# Parent  6de8e7ad95c39f79f96f895e7713486a4a3c39cc
tuned;

diff -r 6de8e7ad95c3 -r 7e020220561a src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Dec 09 20:21:13 2015 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Dec 09 20:58:09 2015 +0100
@@ -242,7 +242,7 @@
 
 fun internal att =
   Token.make_src ("Pure.attribute", Position.none)
-    [Token.make_value "<attribute>" (Token.Attribute att)];
+    [Token.make_string ("<attribute>", Position.none) |> Token.assign (SOME (Token.Attribute att))];
 
 val _ = Theory.setup
   (setup (Binding.make ("attribute", @{here}))
diff -r 6de8e7ad95c3 -r 7e020220561a src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Dec 09 20:21:13 2015 +0100
+++ b/src/Pure/Isar/token.ML	Wed Dec 09 20:58:09 2015 +0100
@@ -13,7 +13,7 @@
     (*delimited content*)
     String | Alt_String | Verbatim | Cartouche | Comment |
     (*special content*)
-    Error of string | Internal_Value | EOF
+    Error of string | EOF
   val str_of_kind: kind -> string
   type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
   type T
@@ -63,7 +63,6 @@
   val text_of: T -> string * string
   val get_files: T -> file Exn.result list
   val put_files: file Exn.result list -> T -> T
-  val make_value: string -> value -> T
   val get_value: T -> value option
   val map_value: (value -> value) -> T -> T
   val name_value: name_value -> value
@@ -120,7 +119,7 @@
   (*delimited content*)
   String | Alt_String | Verbatim | Cartouche | Comment |
   (*special content*)
-  Error of string | Internal_Value | EOF;
+  Error of string | EOF;
 
 val str_of_kind =
  fn Command => "command"
@@ -139,7 +138,6 @@
   | Verbatim => "verbatim text"
   | Cartouche => "text cartouche"
   | Comment => "comment text"
-  | Internal_Value => "internal value"
   | Error _ => "bad input"
   | EOF => "end-of-input";
 
@@ -361,9 +359,6 @@
 
 (* access values *)
 
-fun make_value name v =
-  Token ((name, Position.no_range), (Internal_Value, name), Value (SOME v));
-
 fun get_value (Token (_, _, Value v)) = v
   | get_value _ = NONE;