remove map function names from domain package theory data

--- a/src/HOLCF/Domain.thy	Fri Nov 26 14:13:34 2010 -0800
+++ b/src/HOLCF/Domain.thy	Fri Nov 26 15:24:11 2010 -0800
@@ -340,13 +340,13 @@
   deflation_sprod_map deflation_cprod_map deflation_u_map
 
 setup {*
-  fold Domain_Take_Proofs.add_map_function
-    [(@{type_name cfun}, @{const_name cfun_map}, [true, true]),
-     (@{type_name "sfun"}, @{const_name sfun_map}, [true, true]),
-     (@{type_name ssum}, @{const_name ssum_map}, [true, true]),
-     (@{type_name sprod}, @{const_name sprod_map}, [true, true]),
-     (@{type_name prod}, @{const_name cprod_map}, [true, true]),
-     (@{type_name "u"}, @{const_name u_map}, [true])]
+  fold Domain_Take_Proofs.add_rec_type
+    [(@{type_name cfun}, [true, true]),
+     (@{type_name "sfun"}, [true, true]),
+     (@{type_name ssum}, [true, true]),
+     (@{type_name sprod}, [true, true]),
+     (@{type_name prod}, [true, true]),
+     (@{type_name "u"}, [true])]
 *}
 
 end

--- a/src/HOLCF/Powerdomains.thy	Fri Nov 26 14:13:34 2010 -0800
+++ b/src/HOLCF/Powerdomains.thy	Fri Nov 26 15:24:11 2010 -0800
@@ -42,10 +42,10 @@
   deflation_upper_map deflation_lower_map deflation_convex_map
 
 setup {*
-  fold Domain_Take_Proofs.add_map_function
-    [(@{type_name "upper_pd"}, @{const_name upper_map}, [true]),
-     (@{type_name "lower_pd"}, @{const_name lower_map}, [true]),
-     (@{type_name "convex_pd"}, @{const_name convex_map}, [true])]
+  fold Domain_Take_Proofs.add_rec_type
+    [(@{type_name "upper_pd"}, [true]),
+     (@{type_name "lower_pd"}, [true]),
+     (@{type_name "convex_pd"}, [true])]
 *}
 
 end

--- a/src/HOLCF/Tools/Domain/domain.ML	Fri Nov 26 14:13:34 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain.ML	Fri Nov 26 15:24:11 2010 -0800
@@ -118,14 +118,14 @@
     (* test for free type variables, illegal sort constraints on rhs,
        non-pcpo-types and invalid use of recursive type;
        replace sorts in type variables on rhs *)
-    val map_tab = Domain_Take_Proofs.get_map_tab thy;
+    val rec_tab = Domain_Take_Proofs.get_rec_tab thy;
     fun check_rec rec_ok (T as TFree (v,_))  =
         if AList.defined (op =) sorts v then T
         else error ("Free type variable " ^ quote v ^ " on rhs.")
       | check_rec rec_ok (T as Type (s, Ts)) =
         (case AList.lookup (op =) dtnvs' s of
           NONE =>
-            let val rec_ok' = rec_ok andalso Symtab.defined map_tab s;
+            let val rec_ok' = rec_ok andalso Symtab.defined rec_tab s;
             in Type (s, map (check_rec rec_ok') Ts) end
         | SOME typevars =>
           if typevars <> Ts

--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Nov 26 14:13:34 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Nov 26 15:24:11 2010 -0800
@@ -350,17 +350,17 @@
       (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
         (conjuncts deflation_map_binds deflation_map_thm);
 
-    (* register map functions in theory data *)
+    (* register indirect recursion in theory data *)
     local
-      fun register_map ((dname, map_name), args) =
-          Domain_Take_Proofs.add_map_function (dname, map_name, args);
+      fun register_map (dname, args) =
+        Domain_Take_Proofs.add_rec_type (dname, args);
       val dnames = map (fst o dest_Type o fst) dom_eqns;
       val map_names = map (fst o dest_Const) map_consts;
       fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => [];
       val argss = map args dom_eqns;
     in
       val thy =
-          fold register_map (dnames ~~ map_names ~~ argss) thy;
+          fold register_map (dnames ~~ argss) thy;
     end;
 
     (* register deflation theorems *)

--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Nov 26 14:13:34 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Nov 26 15:24:11 2010 -0800
@@ -55,8 +55,8 @@
   val map_of_typ :
     theory -> (typ * term) list -> typ -> term
 
-  val add_map_function : (string * string * bool list) -> theory -> theory
-  val get_map_tab : theory -> (string * bool list) Symtab.table
+  val add_rec_type : (string * bool list) -> theory -> theory
+  val get_rec_tab : theory -> (bool list) Symtab.table
   val add_deflation_thm : thm -> theory -> theory
   val get_deflation_thms : theory -> thm list
   val map_ID_add : attribute
@@ -119,12 +119,10 @@
 (******************************** theory data *********************************)
 (******************************************************************************)
 
-structure MapData = Theory_Data
+structure Rec_Data = Theory_Data
 (
-  (* constant names like "foo_map" *)
-  (* list indicates which type arguments correspond to map arguments *)
-  (* alternatively, which type arguments allow indirect recursion *)
-  type T = (string * bool list) Symtab.table;
+  (* list indicates which type arguments allow indirect recursion *)
+  type T = (bool list) Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
   fun merge data = Symtab.merge (K true) data;
@@ -142,13 +140,13 @@
   val description = "theorems like foo_map$ID = ID"
 );
 
-fun add_map_function (tname, map_name, bs) =
-    MapData.map (Symtab.insert (K true) (tname, (map_name, bs)));
+fun add_rec_type (tname, bs) =
+    Rec_Data.map (Symtab.insert (K true) (tname, bs));
 
 fun add_deflation_thm thm =
     Context.theory_map (DeflMapData.add_thm thm);
 
-val get_map_tab = MapData.get;
+val get_rec_tab = Rec_Data.get;
 fun get_deflation_thms thy = DeflMapData.get (ProofContext.init_global thy);
 
 val map_ID_add = Map_Id_Data.add;