# HG changeset patch
# User huffman
# Date 1258656334 28800
# Node ID c3fbdff7aed04ee64d40f0df5bc422d16cf26af0
# Parent  481bc899febf64875385865f428a4ca48a873dbf
separate conjuncts of isodefl theorem

diff -r 481bc899febf -r c3fbdff7aed0 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Nov 19 10:27:29 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Nov 19 10:45:34 2009 -0800
@@ -492,6 +492,16 @@
       in
         Goal.prove_global thy [] assms goal tacf
       end;
+    val isodefl_binds = map (Binding.prefix_name "isodefl_") dom_binds;
+    fun conjuncts [] thm = []
+      | conjuncts (n::[]) thm = [(n, thm)]
+      | conjuncts (n::ns) thm = let
+          val thmL = thm RS @{thm conjunct1};
+          val thmR = thm RS @{thm conjunct2};
+        in (n, thmL):: conjuncts ns thmR end;
+    val (isodefl_thms, thy) = thy |>
+      (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.standard))
+        (conjuncts isodefl_binds isodefl_thm);
   in
     thy
   end;