Mercurial Mercurial > repos > isabelle / 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.
src/HOLCF/Tools/Domain/domain_extender.ML
changeset 35519 abf45a91d24d
parent 35518 3b20559d809b
child 35520 f433f18d4c41 
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 14:59:24 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 15:06:02 2010 -0800
@@ -158,8 +158,7 @@
         (Binding.name_of con,  (* FIXME preverse binding (!?) *)
          mx,
          ListPair.map (fn ((lazy,sel,tp),vn) =>
-           mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
-                   Option.map Binding.name_of sel,vn))
+           mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
                       (args, Datatype_Prop.make_tnames (map third args))
         ) : cons;
     val eqs : eq list =
@@ -230,8 +229,7 @@
         (Binding.name_of con,   (* FIXME preverse binding (!?) *)
          mx,
          ListPair.map (fn ((lazy,sel,tp),vn) =>
-           mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
-                   Option.map Binding.name_of sel,vn))
+           mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
                       (args, Datatype_Prop.make_tnames (map third args))
         ) : cons;
     val eqs : eq list =
isabelle