# HG changeset patch
# User wenzelm
# Date 1183803374 -7200
# Node ID 5e6c5388e836710d2a825e986eb17d366a0883fb
# Parent  2d32185530d79ab07da527a121a593ca592bbe90
position: line and name;
tuned operations;

diff -r 2d32185530d7 -r 5e6c5388e836 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat Jul 07 12:16:13 2007 +0200
+++ b/src/Pure/General/markup.ML	Sat Jul 07 12:16:14 2007 +0200
@@ -12,9 +12,8 @@
   val none: T
   val property: string * string -> T -> T
   val nameN: string
-  val add_name: string -> T -> T
-  val posN: string
-  val add_pos: Position.T -> T -> T
+  val pos_lineN: string
+  val pos_nameN: string
   val classN: string
   val class: string -> T
   val tyconN: string
@@ -29,10 +28,6 @@
   val typ: T
   val termN: string
   val term: T
-  val propN: string
-  val prop: T
-  val thmN: string
-  val thm: T
   val keywordN: string
   val keyword: string -> T
   val commandN: string
@@ -53,10 +48,8 @@
 fun property x (name, xs) : T = (name, x :: xs);
 
 val nameN = "name";
-fun add_name x = property (nameN, x);
-
-val posN = "pos";
-fun add_pos x = property (posN, Position.str_of x);
+val pos_lineN = "pos_line";
+val pos_nameN = "pos_name";
 
 
 (* logical entities *)
@@ -85,12 +78,6 @@
 val termN = "term";
 val term = (termN, []);
 
-val propN = "prop";
-val prop = (propN, []);
-
-val thmN = "thm";
-val thm = (thmN, []);
-
 
 (* outer syntax *)