# HG changeset patch
# User lcp
# Date 785543449 -3600
# Node ID 9a973c3ba350f2789f06f073f4d36c0af4dbf3da
# Parent  711e4eb8c21358a92e73ba5e04f82c11519767a4
Pure/term: commented typ_subst_TVars, subst_TVars, subst_Vars, subst_vars

diff -r 711e4eb8c213 -r 9a973c3ba350 src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Nov 21 18:48:03 1994 +0100
+++ b/src/Pure/term.ML	Tue Nov 22 23:30:49 1994 +0100
@@ -382,6 +382,7 @@
 		           Some u => u  |  None => t)
       in  subst t  end;
 
+(*Substitute for type Vars in a type*)
 fun typ_subst_TVars iTs T = if null iTs then T else
   let fun subst(Type(a,Ts)) = Type(a, map subst Ts)
 	| subst(T as TFree _) = T
@@ -389,8 +390,10 @@
             (case assoc(iTs,ixn) of None => T | Some(U) => U)
   in subst T end;
 
+(*Substitute for type Vars in a term*)
 val subst_TVars = map_term_types o typ_subst_TVars;
 
+(*Substitute for Vars in a term; see also envir/norm_term*)
 fun subst_Vars itms t = if null itms then t else
   let fun subst(v as Var(ixn,_)) =
             (case assoc(itms,ixn) of None => v | Some t => t)
@@ -399,6 +402,7 @@
         | subst(t) = t
   in subst t end;
 
+(*Substitute for type/term Vars in a term; see also envir/norm_term*)
 fun subst_vars(iTs,itms) = if null iTs then subst_Vars itms else
   let fun subst(Const(a,T)) = Const(a,typ_subst_TVars iTs T)
         | subst(Free(a,T)) = Free(a,typ_subst_TVars iTs T)