src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 35514 a2cfa413eaab
parent 35512 d1ef88d7de5a
child 35521 47eec4da124a
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 13:01:22 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 13:50:23 2010 -0800
     1.3 @@ -106,7 +106,7 @@
     1.4  let
     1.5  
     1.6  val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
     1.7 -val map_tab = Domain_Isomorphism.get_map_tab thy;
     1.8 +val map_tab = Domain_Take_Proofs.get_map_tab thy;
     1.9  
    1.10  
    1.11  (* ----- getting the axioms and definitions --------------------------------- *)
    1.12 @@ -139,7 +139,7 @@
    1.13  
    1.14  val abs_const = Const(dname^"_abs", rhsT ->> lhsT);
    1.15  
    1.16 -val iso_info : Domain_Isomorphism.iso_info =
    1.17 +val iso_info : Domain_Take_Proofs.iso_info =
    1.18    {
    1.19      absT = lhsT,
    1.20      repT = rhsT,
    1.21 @@ -229,7 +229,7 @@
    1.22  
    1.23  fun comp_theorems (comp_dnam, eqs: eq list) thy =
    1.24  let
    1.25 -val map_tab = Domain_Isomorphism.get_map_tab thy;
    1.26 +val map_tab = Domain_Take_Proofs.get_map_tab thy;
    1.27  
    1.28  val dnames = map (fst o fst) eqs;
    1.29  val conss  = map  snd        eqs;