--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Mar 13 16:48:57 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Mar 13 17:05:34 2010 -0800
@@ -115,8 +115,7 @@
(* ----- define constructors ------------------------------------------------ *)
val (result, thy) =
- Domain_Constructors.add_domain_constructors
- (Long_Name.base_name dname) spec iso_info thy;
+ Domain_Constructors.add_domain_constructors dbind spec iso_info thy;
val con_appls = #con_betas result;
val {exhaust, casedist, ...} = result;