--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Nov 10 18:45:48 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Nov 12 06:05:26 2010 -0800
@@ -406,7 +406,7 @@
: (Domain_Take_Proofs.iso_info list
* Domain_Take_Proofs.take_induct_info) * theory =
let
- val _ = Theory.requires thy "Representable" "domain isomorphisms";
+ val _ = Theory.requires thy "Domain" "domain isomorphisms";
(* this theory is used just for parsing *)
val tmp_thy = thy |>
--- a/src/HOLCF/Tools/repdef.ML Wed Nov 10 18:45:48 2010 -0800
+++ b/src/HOLCF/Tools/repdef.ML Fri Nov 12 06:05:26 2010 -0800
@@ -88,7 +88,7 @@
(thy: theory)
: (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory =
let
- val _ = Theory.requires thy "Representable" "repdefs";
+ val _ = Theory.requires thy "Domain" "repdefs";
(*rhs*)
val tmp_ctxt =