--- a/src/HOLCF/Tools/domain/domain_syntax.ML Sun Mar 01 16:48:06 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_syntax.ML Sun Mar 01 23:36:12 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOLCF/Tools/domain/domain_syntax.ML
- ID: $Id$
Author: David von Oheimb
Syntax generator for domain command.
@@ -22,14 +21,14 @@
else 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;
- fun when_type (_ ,_,args) = foldr (op ->>) (freetvar "t") (map third args);
+ fun when_type (_ ,_,args) = List.foldr (op ->>) (freetvar "t") (map third args);
in
val dtype = Type(dname,typevars);
val dtype2 = foldr1 mk_ssumT (map prod cons');
val dnam = Sign.base_name dname;
val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn);
val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn);
- val const_when = (dnam^"_when",foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
+ val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
val const_copy = (dnam^"_copy", dtypeprod ->> dtype ->> dtype , NoSyn);
end;
@@ -41,7 +40,7 @@
else c::esc cs
| esc [] = []
in implode o esc o Symbol.explode end;
- fun con (name,s,args) = (name,foldr (op ->>) dtype (map third args),s);
+ fun con (name,s,args) = (name, List.foldr (op ->>) dtype (map third args),s);
fun dis (con ,s,_ ) = (dis_name_ con, dtype->>trT,
Mixfix(escape ("is_" ^ con), [], Syntax.max_pri));
(* strictly speaking, these constants have one argument,
@@ -86,7 +85,7 @@
val capp = app "Rep_CFun";
fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args);
fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n);
- fun arg1 n (con,_,args) = foldr cabs (expvar n) (argvars n args);
+ fun arg1 n (con,_,args) = List.foldr cabs (expvar n) (argvars n args);
fun when1 n m = if n = m then arg1 n else K (Constant "UU");
fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];