update Theory.requires with new theory name
authorhuffman
Fri, 12 Nov 2010 06:05:26 -0800
changeset 40510 638943ad5bdc
parent 40506 4c5363173f88
child 40511 094e5d1f5baf
update Theory.requires with new theory name
src/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOLCF/Tools/repdef.ML
--- 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 =