--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Nov 19 16:48:40 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Nov 19 16:50:25 2009 -0800
@@ -12,6 +12,8 @@
(string list * binding * mixfix * string) list -> theory -> theory
val add_type_constructor:
(string * term * string * thm * thm) -> theory -> theory
+ val get_map_tab:
+ theory -> string Symtab.table
end;
structure Domain_Isomorphism :> DOMAIN_ISOMORPHISM =
@@ -68,6 +70,8 @@
#> RepData.map (Thm.add_thm REP_thm)
#> IsodeflData.map (Thm.add_thm isodefl_thm);
+val get_map_tab = MapData.get;
+
(******************************************************************************)
(******************************* building types *******************************)