# HG changeset patch
# User huffman
# Date 1258673479 28800
# Node ID d3616f61c5c4a9ba2aa9d15b8d656a3fbdd24eb7
# Parent  6442aa3773a24fa37b6fdd0889d4ad3c761ac614
rename generated abs_iso, rep_iso lemmas

diff -r 6442aa3773a2 -r d3616f61c5c4 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Nov 19 13:23:58 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Nov 19 15:31:19 2009 -0800
@@ -433,14 +433,16 @@
         val rep_iso_thm = make @{thm domain_rep_iso};
         val abs_iso_thm = make @{thm domain_abs_iso};
         val isodefl_thm = make @{thm isodefl_abs_rep};
-        val rep_iso_bind = Binding.suffix_name "_rep_iso" tbind;
-        val abs_iso_bind = Binding.suffix_name "_abs_iso" tbind;
-        val isodefl_bind = Binding.prefix_name "isodefl_abs_rep_" tbind;
-        val (_, thy) = thy |>
-          (PureThy.add_thms o map Thm.no_attributes)
-            [(rep_iso_bind, rep_iso_thm),
-             (abs_iso_bind, abs_iso_thm),
-             (isodefl_bind, isodefl_thm)];
+        val rep_iso_bind = Binding.name "rep_iso";
+        val abs_iso_bind = Binding.name "abs_iso";
+        val isodefl_bind = Binding.name "isodefl_abs_rep";
+        val (_, thy) = thy
+          |> Sign.add_path (Binding.name_of tbind)
+          |> (PureThy.add_thms o map Thm.no_attributes)
+              [(rep_iso_bind, rep_iso_thm),
+               (abs_iso_bind, abs_iso_thm),
+               (isodefl_bind, isodefl_thm)]
+          ||> Sign.parent_path;
       in
         (((rep_iso_thm, abs_iso_thm), isodefl_thm), thy)
       end;