Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
using types one = unit lift and translations causes troubles between
authorslotosch
Mon, 17 Feb 1997 11:01:10 +0100
changeset 2641 533a84b3bedd
parent 2640 ee4dfce170a0
child 2642 3c3a84cc85a9
using types one = unit lift and translations causes troubles between the type one and the constant one. The later was changed to ONE
src/HOLCF/domain/axioms.ML file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/domain/axioms.ML	Mon Feb 17 10:57:11 1997 +0100
+++ b/src/HOLCF/domain/axioms.ML	Mon Feb 17 11:01:10 1997 +0100
@@ -38,7 +38,7 @@
      fun idxs z x arg = (if is_lazy arg then fn t => %%"up"`t else Id)
 			(if recu andalso is_rec arg then (cproj (Bound z) 
 			(length eqs) (rec_of arg))`Bound(z-x) else Bound(z-x));
-     fun parms [] = %%"one"
+     fun parms [] = %%"ONE"
      |   parms vs = foldr'(fn(x,t)=> %%"spair"`x`t)(mapn (idxs(length vs))1 vs);
      fun inj y 1 _ = y
      |   inj y _ 0 = %%"sinl"`y
isabelle