--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 00:34:26 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 02:28:45 2010 -0800
@@ -209,8 +209,6 @@
if definitional then thy
else fold ax_lub_take dnames thy
end;
-
- val use_copy_def = length eqs>1 andalso not definitional;
in
thy
|> Sign.add_path comp_dnam
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML Tue Mar 02 00:34:26 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Tue Mar 02 02:28:45 2010 -0800
@@ -39,8 +39,6 @@
fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
fun prod (_,args,_) = case args of [] => oneT
| _ => foldr1 mk_sprodT (map opt_lazy args);
- fun freetvar s = let val tvar = mk_TFree s in
- if tvar mem typevars then freetvar ("t"^s) else tvar end;
in
val dtype = Type(dname,typevars);
val dtype2 = foldr1 mk_ssumT (map prod cons');