--- 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