src/HOLCF/Tools/Domain/domain_axioms.ML
changeset 33504 b4210cc3ac97
parent 33396 45c5c3c51918
child 33798 46cbbcbd4e68
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 05 11:36:30 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 05 11:47:00 2009 -0800
@@ -28,11 +28,11 @@
 
 (* FIXME: use theory data for this *)
 val copy_tab : string Symtab.table =
-    Symtab.make [(@{type_name "->"}, @{const_name "cfun_fun"}),
-                 (@{type_name "++"}, @{const_name "ssum_fun"}),
-                 (@{type_name "**"}, @{const_name "sprod_fun"}),
-                 (@{type_name "*"}, @{const_name "cprod_fun"}),
-                 (@{type_name "u"}, @{const_name "u_fun"})];
+    Symtab.make [(@{type_name "->"}, @{const_name "cfun_map"}),
+                 (@{type_name "++"}, @{const_name "ssum_map"}),
+                 (@{type_name "**"}, @{const_name "sprod_map"}),
+                 (@{type_name "*"}, @{const_name "cprod_map"}),
+                 (@{type_name "u"}, @{const_name "u_map"})];
 
 fun copy_of_dtyp r dt = if DatatypeAux.is_rec_type dt then copy r dt else ID
 and copy r (DatatypeAux.DtRec i) = r i