# HG changeset patch
# User huffman
# Date 1267466414 28800
# Node ID d1630f317ed05fae645ffdf6ada9d07557ee0c5c
# Parent  c91854705b1d131f7b9a4420c6ad12f4c0e47b85
qualify constructor names with type name

diff -r c91854705b1d -r d1630f317ed0 src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Mon Mar 01 09:55:32 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Mon Mar 01 10:00:14 2010 -0800
@@ -1025,6 +1025,9 @@
     val rep_defined_iff = iso_locale RS @{thm iso.rep_defined_iff};
     val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff};
 
+    (* qualify constants and theorems with domain name *)
+    val thy = Sign.add_path dname thy;
+
     (* define constructor functions *)
     val (con_result, thy) =
       let
@@ -1047,10 +1050,6 @@
           con_betas casedist iso_locale rep_const thy
       end;
 
-    (* qualify constants and theorems with domain name *)
-    (* TODO: enable this earlier *)
-    val thy = Sign.add_path dname thy;
-
     (* define and prove theorems for selector functions *)
     val (sel_thms : thm list, thy : theory) =
       let