Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_dt_alpha.ML
changeset 2435 3772bb3bd7ce
parent 2431 331873ebc5cd
child 2438 abafea9b39bb 
--- a/Nominal/nominal_dt_alpha.ML	Wed Aug 25 22:55:42 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Wed Aug 25 23:16:42 2010 +0800
@@ -291,7 +291,7 @@
 fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys =
 let
   (* proper import of type-variables does not work,
-     since ther are replaced by new variables, messing
+     since then they are replaced by new variables, messing
      up the ty_term assoc list *)
   val distinct_thms' = map Thm.legacy_freezeT distinct_thms
   val ty_trm_assoc = alpha_tys ~~ alpha_trms
nominal2