# HG changeset patch
# User huffman
# Date 1267632896 28800
# Node ID 119653afcd6e2674a6ac17142ee14aecd0b8b2e1
# Parent  bb088a6fafbce703eb4ca825a96fc8f2a882ec11
remove copy_of_dtyp from domain_axioms.ML

diff -r bb088a6fafbc -r 119653afcd6e src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Wed Mar 03 07:55:52 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Wed Mar 03 08:14:56 2010 -0800
@@ -14,9 +14,6 @@
   val axiomatize_lub_take :
       binding * term -> theory -> thm * theory
 
-  val copy_of_dtyp :
-      string Symtab.table -> (int -> term) -> Datatype.dtyp -> term
-
   val add_axioms :
       (binding * (typ * typ)) list -> theory ->
       Domain_Take_Proofs.iso_info list * theory
@@ -26,32 +23,6 @@
 structure Domain_Axioms : DOMAIN_AXIOMS =
 struct
 
-(* TODO: move copy_of_dtyp somewhere else! *)
-local open Domain_Library in
-
-infixr 0 ===>;infixr 0 ==>;infix 0 == ; 
-infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<;
-infix 9 `   ; infix 9 `% ; infix 9 `%%; infixr 9 oo;
-
-(* FIXME: use theory data for this *)
-val copy_tab : string Symtab.table =
-    Symtab.make [(@{type_name cfun}, @{const_name "cfun_map"}),
-                 (@{type_name ssum}, @{const_name "ssum_map"}),
-                 (@{type_name sprod}, @{const_name "sprod_map"}),
-                 (@{type_name "*"}, @{const_name "cprod_map"}),
-                 (@{type_name "u"}, @{const_name "u_map"})];
-
-fun copy_of_dtyp tab r dt =
-    if Datatype_Aux.is_rec_type dt then copy tab r dt else ID
-and copy tab r (Datatype_Aux.DtRec i) = r i
-  | copy tab r (Datatype_Aux.DtTFree a) = ID
-  | copy tab r (Datatype_Aux.DtType (c, ds)) =
-    case Symtab.lookup tab c of
-      SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
-    | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
-
-end; (* local open *)
-
 open HOLCF_Library;
 
 fun axiomatize_isomorphism
diff -r bb088a6fafbc -r 119653afcd6e src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Mar 03 07:55:52 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Mar 03 08:14:56 2010 -0800
@@ -160,12 +160,21 @@
   fun get_deflation_take dn = PureThy.get_thm thy (dn ^ ".deflation_take");
   val axs_deflation_take = map get_deflation_take dnames;
 
+  fun copy_of_dtyp tab r dt =
+      if Datatype_Aux.is_rec_type dt then copy tab r dt else ID
+  and copy tab r (Datatype_Aux.DtRec i) = r i
+    | copy tab r (Datatype_Aux.DtTFree a) = ID
+    | copy tab r (Datatype_Aux.DtType (c, ds)) =
+      case Symtab.lookup tab c of
+        SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
+      | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
+
   fun one_take_app (con, args) =
     let
       fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
       fun one_rhs arg =
           if Datatype_Aux.is_rec_type (dtyp_of arg)
-          then Domain_Axioms.copy_of_dtyp map_tab
+          then copy_of_dtyp map_tab
                  mk_take (dtyp_of arg) ` (%# arg)
           else (%# arg);
       val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args);