src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 33801 e8535acd302c
parent 33504 b4210cc3ac97
child 33810 38375b16ffd9
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Nov 19 16:48:40 2009 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Nov 19 16:50:25 2009 -0800
     1.3 @@ -141,6 +141,8 @@
     1.4  
     1.5  val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
     1.6  val pg = pg' thy;
     1.7 +val map_tab = Domain_Isomorphism.get_map_tab thy;
     1.8 +
     1.9  
    1.10  (* ----- getting the axioms and definitions --------------------------------- *)
    1.11  
    1.12 @@ -599,7 +601,8 @@
    1.13        val lhs = dc_copy`%"f"`(con_app con args);
    1.14        fun one_rhs arg =
    1.15            if DatatypeAux.is_rec_type (dtyp_of arg)
    1.16 -          then Domain_Axioms.copy_of_dtyp (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
    1.17 +          then Domain_Axioms.copy_of_dtyp map_tab
    1.18 +                 (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
    1.19            else (%# arg);
    1.20        val rhs = con_app2 con one_rhs args;
    1.21        val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
    1.22 @@ -660,6 +663,7 @@
    1.23  fun comp_theorems (comp_dnam, eqs: eq list) thy =
    1.24  let
    1.25  val global_ctxt = ProofContext.init thy;
    1.26 +val map_tab = Domain_Isomorphism.get_map_tab thy;
    1.27  
    1.28  val dnames = map (fst o fst) eqs;
    1.29  val conss  = map  snd        eqs;
    1.30 @@ -727,7 +731,8 @@
    1.31            fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
    1.32            fun one_rhs arg =
    1.33                if DatatypeAux.is_rec_type (dtyp_of arg)
    1.34 -              then Domain_Axioms.copy_of_dtyp mk_take (dtyp_of arg) ` (%# arg)
    1.35 +              then Domain_Axioms.copy_of_dtyp map_tab
    1.36 +                     mk_take (dtyp_of arg) ` (%# arg)
    1.37                else (%# arg);
    1.38            val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args);
    1.39            val rhs = con_app2 con one_rhs args;