# HG changeset patch # User wenzelm # Date 1112860277 -7200 # Node ID 4a1d07bb53e2a630df859591ee8ed2e29765b328 # Parent 60c56561bcf481e3c3aea3c03b3e845883463d42 reverted renaming of Some/None in comments and strings; diff -r 60c56561bcf4 -r 4a1d07bb53e2 TFL/dcterm.ML --- a/TFL/dcterm.ML Thu Apr 07 09:28:16 2005 +0200 +++ b/TFL/dcterm.ML Thu Apr 07 09:51:17 2005 +0200 @@ -71,7 +71,7 @@ (*--------------------------------------------------------------------------- - * SOME simple constructor functions. + * Some simple constructor functions. *---------------------------------------------------------------------------*) val mk_hol_const = Thm.cterm_of (Theory.sign_of HOL.thy) o Const; diff -r 60c56561bcf4 -r 4a1d07bb53e2 src/ZF/Tools/cartprod.ML --- a/src/ZF/Tools/cartprod.ML Thu Apr 07 09:28:16 2005 +0200 +++ b/src/ZF/Tools/cartprod.ML Thu Apr 07 09:51:17 2005 +0200 @@ -61,7 +61,7 @@ functor CartProd_Fun (Pr: PR) : CARTPROD = struct -(* SOME of these functions expect "pseudo-types" containing products, +(* Some of these functions expect "pseudo-types" containing products, as in HOL; the true ZF types would just be "i" *) fun mk_prod (T1,T2) = Type("*", [T1,T2]);