# HG changeset patch
# User wenzelm
# Date 1408608426 -7200
# Node ID d41e3d0ac50c7c1d9c86efbbb21c212a84fe065b
# Parent  ff55b42303bc1f2666c656f10bddad04d63a9b45
tuned;

diff -r ff55b42303bc -r d41e3d0ac50c src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Aug 21 09:48:59 2014 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Aug 21 10:07:06 2014 +0200
@@ -214,7 +214,9 @@
 
 (* internal attribute *)
 
-fun internal att = Token.src ("Pure.attribute", Position.none) [Token.mk_attribute att];
+fun internal att =
+  Token.src ("Pure.attribute", Position.none)
+    [Token.make_value "<attribute>" (Token.Attribute att)];
 
 val _ = Theory.setup
   (setup (Binding.make ("attribute", @{here}))
diff -r ff55b42303bc -r d41e3d0ac50c src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Thu Aug 21 09:48:59 2014 +0200
+++ b/src/Pure/Isar/token.ML	Thu Aug 21 10:07:06 2014 +0200
@@ -66,14 +66,10 @@
   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 reports_of_value: T -> Position.report list
-  val mk_name: string -> T
-  val mk_typ: typ -> T
-  val mk_term: term -> T
-  val mk_fact: string option * thm list -> T
-  val mk_attribute: (morphism -> attribute) -> T
   val transform: morphism -> T -> T
   val transform_src: morphism -> src -> src
   val init_assignable: T -> T
@@ -380,6 +376,9 @@
 
 (* access values *)
 
+fun make_value name v =
+  Token ((name, Position.no_range), (InternalValue, name), Value (SOME v));
+
 fun get_value (Token (_, _, Value v)) = v
   | get_value _ = NONE;
 
@@ -400,17 +399,6 @@
   | _ => []);
 
 
-(* make values *)
-
-fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
-
-val mk_name = mk_value "<name>" o name0;
-val mk_typ = mk_value "<typ>" o Typ;
-val mk_term = mk_value "<term>" o Term;
-val mk_fact = mk_value "<fact>" o Fact;
-val mk_attribute = mk_value "<attribute>" o Attribute;
-
-
 (* transform *)
 
 fun transform phi =