src/Pure/term.ML

 
 (*Indexnames can be quickly renamed by adding an offset to the integer part,
   for resolution.*)
 type indexname = string*int;
 
-(* Types are classified by classes. *)
+(* Types are classified by sorts. *)
 type class = string;
 type sort  = class list;
 
 (* The sorts attached to TFrees and TVars specify the sort of that variable *)
 datatype typ = Type  of string * typ list

 val op ---> = foldr (op -->);
 
 
 (*terms.  Bound variables are indicated by depth number.
   Free variables, (scheme) variables and constants have names.
-  An term is "closed" if there every bound variable of level "lev"
+  An term is "closed" if every bound variable of level "lev"
   is enclosed by at least "lev" abstractions. 
 
   It is possible to create meaningless terms containing loose bound vars
   or type mismatches.  But such terms are not allowed in rules. *)
 

   | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
   | loose_bvar1 _ = false;
 
 (*Substitute arguments for loose bound variables.
   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
-  Note that for ((x,y)c)(a,b), the bound vars in c are x=1 and y=0
+  Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
 	and the appropriate call is  subst_bounds([b,a], c) .
   Loose bound variables >=n are reduced by "n" to
      compensate for the disappearance of lambdas.
 *)
 fun subst_bounds (args: term list, t) : term = 

 
 (*insertion into list, optimized version for indexnames*)
 fun ins_ix (x,xs) = if mem_ix (x, xs) then xs else x :: xs;
 
 (*Tests whether 2 terms are alpha-convertible and have same type.
-  Note that constants and Vars may have more than one type.*)
+  Note that constants may have more than one type.*)
 fun (Const(a,T)) aconv (Const(b,U)) = a=b  andalso  T=U
   | (Free(a,T))  aconv (Free(b,U))  = a=b  andalso  T=U
   | (Var(v,T))   aconv (Var(w,U))   = eq_ix(v,w)  andalso  T=U
   | (Bound i)    aconv (Bound j)    = i=j
   | (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u  andalso  T=U

 
 
 (**** Syntax-related declarations ****)
 
 
-(*Dummy type for parsing.  Will be replaced during type inference. *)
+(*Dummy type for parsing and printing.  Will be replaced during type inference. *)
 val dummyT = Type("dummy",[]);
 
 (*scan a numeral of the given radix, normally 10*)
 fun scan_radixint (radix: int, cs) : int * string list =
   let val zero = ord"0"