tuned;
authorwenzelm
Wed, 20 May 1998 18:55:16 +0200
changeset 4948 c53aa26ccfd2
parent 4947 15fd948d6c69
child 4949 c73f72daee64
tuned;
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 *)