# HG changeset patch
# User wenzelm
# Date 895683316 -7200
# Node ID c53aa26ccfd217bee908179901fd49c4307ce812
# Parent  15fd948d6c69c6392082e784a53ac5b122fa30fd
tuned;

diff -r 15fd948d6c69 -r c53aa26ccfd2 src/Pure/Thy/position.ML
--- a/src/Pure/Thy/position.ML	Wed May 20 15:20:28 1998 +0200
+++ b/src/Pure/Thy/position.ML	Wed May 20 18:55:16 1998 +0200
@@ -7,12 +7,12 @@
 
 signature POSITION =
 sig
-  eqtype T
+  type T
   val none: T
   val line: int -> T
   val name: string -> T
   val line_name: int -> string -> T
-  val incr: T -> T
+  val inc: T -> T
   val str_of: T -> string
 end;
 
@@ -31,10 +31,10 @@
 fun line_name n s = Pos (Some n, Some s);
 
 
-(* incr *)
+(* increment *)
 
-fun incr (pos as Pos (None, _)) = pos
-  | incr (Pos (Some n, opt_s)) = Pos (Some (n + 1), opt_s);
+fun inc (pos as Pos (None, _)) = pos
+  | inc (Pos (Some n, opt_s)) = Pos (Some (n + 1), opt_s);
 
 
 (* str_of *)