# HG changeset patch # User huffman # Date 1258661149 28800 # Node ID 002e0e0173114799b19e7edde7a09e34d3d48118 # Parent fef59343b4b3b22c30f0ef561f52fc712cb7010b change Theory.requires diff -r fef59343b4b3 -r 002e0e017311 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Nov 19 11:54:23 2009 -0800 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Nov 19 12:05:49 2009 -0800 @@ -307,7 +307,7 @@ (thy: theory) : theory = let - val _ = Theory.requires thy "Domain" "domain definitions"; + val _ = Theory.requires thy "Representable" "domain isomorphisms"; (* this theory is used just for parsing *) val tmp_thy = thy |>